Name
Abstract | ||
|---|---|---|
Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification. In this paper, we explore the overlap between formal verification and code optimization. We propose two approaches to reuse the invariants derived in formal proofs and integrate them into compilation. The first applies invariants extracted from the proof, while the second leverages the property of program safety (i.e., the absence of bugs). We reuse this information to improve the performance of generated object code. We evaluated these methods on seL4, a real-world formally-verified microkernel, and obtained improvements in average runtime performance (up to 28%) and in worst-case execution time (up to 25%). In macro-benchmarks, we found the performance of para-virtualized Linux running on the microkernel improved by 6-16%. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2509136.2509513 | OOPSLA |
Keywords | Field | DocType |
code optimization,average runtime performance,formal proof,object code,mathematical proof,program safety,program invariants,formal program verification,code adheres,formal verification,optimization | Program optimization,Object code,Programming language,Reuse,Computer science,Correctness,Microkernel,Theoretical computer science,Mathematical proof,Invariant (mathematics),Formal verification | Conference |
Volume | Issue | ISSN |
48 | 10 | 0362-1340 |
Citations | PageRank | References |
1 | 0.35 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yao Shi | 1 | 124 | 13.96 |
| Bernard Blackham | 2 | 69 | 4.41 |
| Gernot Heiser | 3 | 2525 | 137.42 |