Name
Abstract | ||
|---|---|---|
We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties.We report on our experience in applying the techniques in an extensive (100,000 lines of proof) case study--the formal verification of an executable model of the seL4 operating system microkernel. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-71067-7_16 | TPHOLs |
Keywords | Field | DocType |
nondeterministic state monad,single proof,state monads,full generality,large-scale verification,executable model,complex property,large program,scalable refinement,case study,monad calculus,secure microkernels,formal verification,two dimensions,functional programming,operating system,hoare logic | Programming language,Nondeterministic algorithm,Refinement calculus,Computer science,Hoare logic,Algorithm,Microkernel,Theoretical computer science,Monad (functional programming),Executable,Formal verification,Scalability | Conference |
Volume | ISSN | Citations |
5170 | 0302-9743 | 43 |
PageRank | References | Authors |
2.36 | 12 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David Cock | 1 | 827 | 37.44 |
| Gerwin Klein | 2 | 1450 | 87.47 |
| Thomas Sewell | 3 | 914 | 37.60 |