Formal reasoning about programs is one of the oldest and most fundamental research directions in computer science. It has also been one of the most elusive.
Continuous Reasoning: Scaling the impact of formal methods
Loading Video...
There has been a tremendous amount of valuable research in formal methods, but rarely have formal reasoning techniques been deployed as part of the development process of large industrial codebases.
This talk describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers. We describe our experience using continuous reasoning with large, rapidly changing codebases at Facebook, and we describe open problems and directions for research for the scientific community.
This a paper with the same title accompanying this talk appears in the LICS’18 proceedings.
People:
Oxford Unit:
Keywords:
More in this Series...
During the past 50 years there has been extensive, continuous, and increasing interaction between logic and computer science.
In many respects, logic provides computer science with both a unifying foundational framework and a modelling tool. Indeed, logic has rightly been called 'the calculus of computer science," playing a crucial role in such diverse areas as artificial intelligence, computational complexity, distributed computing, database systems, hardware design,...
Subscribe
Download Media
- Video (616.12 MB)