Towards making formal methods normal: meeting developers where they are
Formal verification of software has a reputation of being a niche and heroic activity; it is only applied to systems of particular sensitivity and is performed by verification engineers with specialized skills to produce software with unusually high level of assurance. This paper considers whether it would be possible to increase adoption of formal methods by melding it with developers’ existing practices and workflows. We do not believe that widespread adoption will follow from evangelizing the prevailing formal methods argument that correct software is more important than engineering teams realize. Instead, our focus is on what we would need to do to show programmers that formal verification tools can offer a higher level of assurance without the heroics. We do this by considering how we might make verification tooling that both serves developers’ needs and fits easily into their existing development lifecycle. We propose a target of 2-3 orders of magnitude increase in adoption within a decade driven by ensuring a positive ‘weekly cost:benefit’ ratio for developer time invested.
Wed 18 Nov Times are displayed in time zone: Central Time (US & Canada) change
|11:00 - 11:20|
|11:20 - 11:40|
April GonçalvesMetastate AGPre-print
|11:40 - 12:00|
Alastair ReidArm Ltd, Luke ChurchUniversity of Cambridge, Shaked FlurGoogle Research, Sarah de HaasGoogle Research, Maritza JohnsonGoogle Research, Ben LaurieGoogle ResearchLink to publication