TY - JOUR
T1 - QED at large
T2 - A survey of engineering of formally verified software
AU - Ringer, Talia
AU - Palmskog, Karl
AU - Sergey, Ilya
AU - Gligoric, Milos
AU - Tatlock, Zachary
N1 - Funding Information:
We would like to thank Dan Grossman, Derek Dreyer, Xavier Leroy, Benjamin Pierce, Andrew Appel, Bob Harper, Jonathan Aldrich, Karl Crary, Adam Chlipala, Chris Martens, Joachim Breitner, Christine Rizkallah, Giuliano Losa, Thomas Tuerk, Roberto Guanciale, DougWoos, James R. Wilcox, Ryan Doenges, Jared Roesch, Sorin Lerner, Leslie Lamport, Fred Schneider, John Leo, Bob Atkey, Lars Hupel, Buday Gergely, Makarius Wenzel, Jasmin Christian Blanchette, Matthieu Sozeau, Cyril Cohen, David Thrane Christiansen, Sam Tobin-Hochstadt, Mario Alvarez, Joomy Korkut, Robert Rand, Taylor Blau, Anna Kornfeld Simpson, Jonathan Sterling, Colin Barret, Toby Murray, Gerwin Klein, Graydon Hoare, Emilio Jesus Gallego Arias, and Brendan Zabarauskas. We are grateful to the anonymous reviewers for their detailed comments and valuable suggestions. This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-1256082, the National Science Foundation under Grant Nos. CCF-1652517, CCF-1836813, and CCF-1749570, and by a Research Award from Facebook. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
Publisher Copyright:
© 2019 Institute of Electrical and Electronics Engineers Inc.. All rights reserved.
PY - 2019/9/3
Y1 - 2019/9/3
N2 - Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been available for over 40 years, but have only recently seen wide practical use. Projects based on construction of machine-checked formal proofs are now reaching an unprecedented scale, comparable to large software projects, which leads to new challenges in proof development and maintenance. Despite its increasing importance, the field of proof engineering is seldom considered in its own right; related theories, techniques, and tools span many fields and venues. This survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development.
AB - Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been available for over 40 years, but have only recently seen wide practical use. Projects based on construction of machine-checked formal proofs are now reaching an unprecedented scale, comparable to large software projects, which leads to new challenges in proof development and maintenance. Despite its increasing importance, the field of proof engineering is seldom considered in its own right; related theories, techniques, and tools span many fields and venues. This survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development.
UR - http://www.scopus.com/inward/record.url?scp=85071915948&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85071915948&partnerID=8YFLogxK
U2 - 10.1561/2500000045
DO - 10.1561/2500000045
M3 - Article
AN - SCOPUS:85071915948
SN - 2325-1107
VL - 5
SP - 102
EP - 281
JO - Foundations and Trends in Programming Languages
JF - Foundations and Trends in Programming Languages
IS - 2-3
ER -