Towards making formal methods normal - meeting developers where they are

Alastair Reid, Luke Church, Shaked Flur, Sarah de Haas, Maritza Johnson, Ben Laurie

[pdf] [slides] [video] [url]

arXiv:2010.16345 [cs.LO]
October 2020

Abstract

Formal verification of software is a bit of a niche activity: it is only applied to the most safety-critical or security-critical software and it is typically only performed by specialized verification engineers. This paper considers whether it would be possible to increase adoption of formal methods by integrating formal methods with developers’ existing practices and workflows.

We do not believe that widespread adoption will follow from making the prevailing formal methods argument that correctness is more important than engineering teams realize. Instead, our focus is on what we would need to do to enable programmers to make effective use of formal verification tools and techniques. We do this by considering how we might make verification tooling that both serves developers' needs and fits into their existing development lifecycle. We propose a target of two orders of magnitude increase in adoption within a decade driven by ensuring a positive `weekly cost-benefit' ratio for developer time invested.

First page of paper

BibTeX

@misc{reid:hatra:2020 , abstract = {Formal verification of software is a bit of a niche activity: it is only applied to the most safety-critical or security-critical software and it is typically only performed by specialized verification engineers. This paper considers whether it would be possible to increase adoption of formal methods by integrating formal methods with developers' existing practices and workflows.

We do not believe that widespread adoption will follow from making the prevailing formal methods argument that correctness is more important than engineering teams realize. Instead, our focus is on what we would need to do to enable programmers to make effective use of formal verification tools and techniques. We do this by considering how we might make verification tooling that both serves developers' needs and fits into their existing development lifecycle. We propose a target of two orders of magnitude increase in adoption within a decade driven by ensuring a positive `weekly cost-benefit' ratio for developer time invested.} , ar_file = {HATRA_20} , ar_shortname = {HATRA 20} , archiveprefix = {arXiv} , author = {Alastair Reid and Luke Church and Shaked Flur and Sarah de Haas and Maritza Johnson and Ben Laurie} , day = {30} , eprint = {2010.16345} , file = {hatra2020.pdf} , link = {https://research.google/pubs/pub49713/} , month = {October} , note = {Accepted at HATRA 2020} , png = {hatra2020.png} , primaryclass = {cs.LO} , slides = {hatra2020-slides.pdf} , title = {{T}owards making formal methods normal: meeting developers where they are} , url = {https://research.google/pubs/pub49713/} , video = {https://youtu.be/fUNYvUMSmq4?t=520} , year = {2020} }