PhD defence : Proof-oriented domain-specific language design for high-assurance software
Channel: Denis Merigoux
Date: 22/12/2021

My PhD defence took place on Monday, December 13th at 3pm in the Jacques-Louis Lions room of building C of the Inria Paris center, 2 rue Simone Iff 75012 Paris.

Here is the abstract of my dissertation:

Program verification consists in analyzing a computer program as a formal artifact  in order to prove the absence of certain categories of bugs before execution.  But to use a program verification framework, one has to first translate the  original source code of the program to verify in the formal language of the  framework. Moreover, one might use different verification frameworks to  prove increasingly specialized properties about the program.  To answer the need for multiple translations of the source program to various  program verification frameworks with different proof paradigms, we advocate  for the use of proof-oriented domain-specific languages. These domain-specific language  should act as a frontend to proof backends, with a language design that  incorporates and distributes the proof obligations between provers.  Moreover, the original program has often already been translated  from informal domain-specific requirements that act as its specification.  To close the top layer of the chain of trust, we claim that proof-oriented  domain-specific language can help domain experts review the program specification  at the base of formally verified implementation developments.  This dissertations discusses the design and usefulness of proof-oriented  domain-specific languages in five case studies. These case studies range  from the domain of cryptographic implementations to legal expert systems,  and often target real-world high-assurance software.  Each of the case study gives its name to a chapter of this dissertation.  Signal* is a verified implementation of the Signal cryptographic protocol  for the Web.Hacspec is a domain-specific language for cryptographic  specifications in Rust. Steel is a separation-logic-powered program verification framework  for the F* proof assistant. Mlang is a compiler for a tax computation domain-specific  language used by the French tax authority. Finally, Catala is a novel language  for encoding legislative specifications into executable and analyzable artifacts.