Synthesis by Fiat
|Event Date:||March 1, 2016|
|Speaker:||Dr. Benjamin Delaware|
|Speaker Affiliation:||Massachusetts Institute of Technology|
|Contact Name:||Professor Sam Midkiff
|Open To:||ACCEPTABLE FOR ECE 694
Software reliability is growing increasingly important as we rely on computers to power our financial system, control our medical devices, and drive our cars. One approach to writing correct software is to let the programming language do more of the work, freeing programmers to work at higher levels of abstraction by trusting the language to enforce those abstractions. A natural consequence of this approach has been the rise of program synthesis, wherein users specify the requirements of a program at a high level and rely on a synthesizer to generate an implementation meeting those requirements. This approach forces users to place a great deal of trust in the synthesizer, preventing them from modifying or extending it when a satisfactory implementation can’t be found. As a consequence, users are forced to program in lower-level languages and rely on other techniques to ensure correctness.
In this talk, I present an approach to synthesis that allows users to inject their own insights without sacrificing correctness. This approach is realized as the Fiat deductive synthesis framework, which uses the Coq proof assistant to provide machine-checked proofs that generated implementations meet users’ original specifications. In Fiat, users write high-level specifications of abstract data types using Coq’s expressive logic; these specifications are then automatically transformed into efficient implementations generating a proof trail along the way that justifying its correctness. Utilizing a verified compiler, Fiat can produce correct-by-construction assembly code which can be linked against other verified assembly modules to build certified, high-assurance software suitable for embedded systems.
Benjamin Delaware is currently a Research Scientist in the Computer Science and Artificial Intelligence Laboratory at MIT, working in the Programming Languages & Verification Group. Prior to coming to MIT, Dr. Delaware received his Ph.D. in Computer Science from the University of Texas at Austin in 2013 under the direction of William Cook. His research focuses on the design and implementation of programming languages and tools that provide higher assurance with lower effort through the use of mechanized theorem provers.