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
Abstract
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
TBD
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