Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification

Formal verification can provide the highest degree of software assurance. Demand for it is growing, but there are still few projects that have successfully applied it to sizeable, real-world systems. This lack of experience makes it hard to predict the size, effort and duration of verification proje...

Full description

Saved in:
Bibliographic Details
Main Authors: Matichuk, Daniel, Murray, Toby, Andronick, June, Jeffery, Ross, Klein, Gerwin, Staples, Mark
Format: Conference Proceeding
Language:English
Subjects:
Approximation methods
Complexity theory
Estimation
formal verification
Isabelle
Mathematical model
proof engineering
seL4
Size measurement
Software
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal verification can provide the highest degree of software assurance. Demand for it is growing, but there are still few projects that have successfully applied it to sizeable, real-world systems. This lack of experience makes it hard to predict the size, effort and duration of verification projects. In this paper, we aim to better understand possible leading indicators of proof size. We present an empirical analysis of proofs from the landmark formal verification of the seL4 microkernel and the two largest software verification proof developments in the Archive of Formal Proofs. Together, these comprise 15,018 individual lemmas and approximately 215,000 lines of proof script. We find a consistent quadratic relationship between the size of the formal statement of a property, and the final size of its formal proof in the interactive theorem prover Isabelle. Combined with our prior work, which has indicated that there is a strong linear relationship between proof effort and proof size, these results pave the way for effort estimation models to support the management of large-scale formal verification projects.
ISSN:0270-5257
1558-1225
DOI:10.1109/ICSE.2015.85