SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 11:40 - 12:00 at SPLASH-IV - Formal Methods Chair(s): Michael Coblenz

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 - 12:20: Formal MethodsHATRA at SPLASH-IV
Chair(s): Michael CoblenzUniversity of Maryland at College Park
11:00 - 11:20
Meeting
HATRA
11:20 - 11:40
Talk
HATRA
April GonçalvesMetastate AG
Pre-print
11:40 - 12:00
Talk
HATRA
Alastair ReidArm Ltd, Luke ChurchUniversity of Cambridge, Shaked FlurGoogle Research, Sarah de HaasGoogle Research, Maritza JohnsonGoogle Research, Ben LaurieGoogle Research
Link to publication