Paper Info
Title
Large-scale formal verification in practice: a process perspective
Abstract
The L4.verified project was a rare success in large-scale, formal verification: it provided a formal, machine-checked, code-level proof of the full functional correctness of the seL4 microkernel. In this paper we report on the development process and management issues of this project, highlighting key success factors. We formulate a detailed descriptive model of its middle-out development process, and analyze the evolution and dependencies of code and proof artifacts. We compare our key findings on verification and re-verification with insights from other verification efforts in the literature. Our analysis of the project is based on complete access to project logs, meeting notes, and version control data over its entire history, including its long-term, ongoing maintenance phase. The aim of this work is to aid understanding of how to successfully run large-scale formal software verification projects.
Year
DOI
Venue
2012
10.1109/ICSE.2012.6227120
ICSE
Keywords
Field
DocType
process perspective,proof artifact,code-level proof,large-scale formal verification,development process,key finding,key success factor,middle-out development process,rare success,verification effort,large-scale formal software verification,formal verification,kernel,maintenance engineering,version control,formal methods,computer bugs,prototypes,formal method,software process,software verification
Critical success factor,Functional verification,Software engineering,Systems engineering,Computer science,Software bug,Correctness,Software development process,Formal methods,Formal verification,Software verification
Conference
Volume
ISSN
ISBN
2
0270-5257
978-1-4673-1067-3
Citations 
PageRank 
References 
9
0.67
20
Authors
7
Name
Order
Citations
PageRank
June Andronick190342.66
Ross Jeffery264742.18
Gerwin Klein3145087.47
Rafal Kolanski480234.23
Mark Staples551538.02
He Zhang681765.63
Liming Zhu793377.31