Name
Abstract | ||
|---|---|---|
Large-scale verification projects pose particular challenges. Issues include proof exploration, efficiency of the edit-check cycle, and proof refactoring for documentation and maintainability. We draw on insights from two large-scale verification projects, L4.verified and Verisoft, that both used the Isabelle/HOL prover. We identify the main challenges in large-scale proofs, propose possible solutions, and discuss the Levity tool, which we developed to automatically move lemmas to appropriate theories, as an example of the kind of tool required by such proofs. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-31374-5_3 | AISC/MKM/Calculemus |
Keywords | Field | DocType |
hol prover,possible solution,appropriate theory,particular challenge,levity tool,large-scale proof,edit-check cycle,main challenge,proof exploration,large-scale verification project,interactive theorem proving | HOL,Programming language,Computer science,Automated proof checking,Algorithm,Theoretical computer science,Mathematical proof,Documentation,Code refactoring,Gas meter prover,Maintainability,Proof assistant | Conference |
Citations | PageRank | References |
11 | 0.59 | 12 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Timothy Bourke | 1 | 113 | 12.71 |
| Matthias Daum | 2 | 11 | 0.59 |
| Gerwin Klein | 3 | 1450 | 87.47 |
| Rafal Kolanski | 4 | 802 | 34.23 |