The 2020 Expert Survey on Formal Methods

Hubert Garavel, Maurice H. ter Beek, and Jaco van de Pol

Formal Methods for Industrial Critical Systems, FMICS 2020. Springer LNCS vol 12327, pp. 3--69


Organised to celebrate the 25th anniversary of the FMICS international conference, the present survey addresses 30 questions on the past, present, and future of formal methods in research, industry, and education. Not less than 130 high-profile experts in formal methods (among whom three Turing award winners and many recipients of other prizes and distinctions) accepted to participate in this survey. We analyse their answers and comments, and present a collection of 111 position statements provided by these experts. The survey is both an exercise in collective thinking and a family picture of key actors in formal methods.

Position Statement

As the abstract says, the paper reports a survey and provides position statements. I was one of the participants and here is my position statement.

Formal methods allow us to calculate properties of computational systems, just as compu- tational fluid dynamics allow us to calculate the flow of air over a wing. The challenge is, and always has been, to automate this efficiently. With modern SMT solvers that can deal with quantified formulas, nonlinear arithmetic, and complex data types, we are almost there. The next challenge is effective use of these capabilities and here I see two big opportunities. First is to embed them, invisibly, inside every tool for software, hardware, and system devel- opment with a view to improving their fault detection and, consequently, their productivity and the quality of the artifacts produced. Second is to find contributions to the predictability and safety of modern autonomous systems largely driven by machine learning and AI.

Springer link to paper

BibTeX Entry


Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page