Abstract:

Formal verification of large software has been an illusive target, riddled with the problem of scalability. Even if the obstacle of scale may be cleared, major challenges remain to adopt formal verification in practice. This paper presents an empirical study using a top-rated formal verification tool for Linux, and draws insights from the study to discuss the intrinsic challenges for adopting formal verification in practice. We discuss challenges that focus on practical needs: (a) facilitate crosschecking of verification results, (b) enable the use of formal verification for certification, and (c) integrate formal methods in a development environment. Leaning on visionary papers by Turing Award recipients, we present novel ideas for advancing formal verification in new directions that would help practicing engineers.

Venue: Formal Verification for Practicing Engineers (FVPE) hosted at the 27th International Symposium on Software Reliability Engineering (ISSRE 2016), Ottawa, Canada

Authors: Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi

Paper (PDF): Insights-FVPE2016.pdf