|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Bedrock: A Software Development Ecosystem Inside a Proof Assistant
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.
This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending
The benefits of formal correctness proofs for software are clear intuitively, but the high human costs of proof construction have generally been viewed as prohibitive. The speaker believes that pervasive verification of deep theorems about software will never be common until formal methods are integrated within the software development process. To support that integration, we need to rethink the familiar programming toolchains. The new world needn’t be all about doing prodigious extra work to achieve the virtue of correct programs; formal methods also suggest new programming approaches that better support abstraction and modularity than do coarser-grained specification styles like normal static types.
This talk overviews Bedrock, a framework for certified programming inside of the Coq proof assistant. Bedrock programs are implemented, specified, verified, and compiled inside of Coq. A single program may be divided into modules with formal interfaces, written in different programming languages and verified with different proof styles. The common foundation is an assembly language with an operational semantics (serving as the trusted code base) and a semantic module system (orchestrating linking of code and proofs across source languages). A few different programming styles have been connected to the shared foundation, including a C-like language with an “array of bytes” memory model, higher-level more C++-like languages with “array of abstract data types” memory models, a domain-specific language for XML processing, standard Coq functional programs, and even declarative specifications that are refined automatically into assembly code with correctness proofs.
The talk will present Bedrock’s shared foundation and sketch the pieces that go into refining declarative specifications into closed assembly programs, covering joint work with Thomas Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory Malecha, Clément Pit—Claudel, and Peng Wang
This talk is part of the Microsoft Research Cambridge, public talks series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsInference Group Babbage Seminar Series
Other talksProduct Market Competition and Option Prices Tales from the Fen Edge: past environments. peat, marl and mud Calabi-Yau volumes and Reflexive Polytopes CERF Cavalcade Security and Privacy in Machine Learning Evolutionary analysis on barcode NGS swine influenza virus data