Name
Abstract | ||
|---|---|---|
The Verisoft project aims at the pervasive formal verification from the application layer over the system level software, comprising a microkernel and a compiler, down to the hardware. The different layers of the system give rise to various abstraction levels to conduct the reasoning steps efficiently. The lower the abstraction level the more details and invariants are necessary to ensure overall system correctness. Illustrated by a page-fault handler we discuss the layers and the trade-off between efficiency of reasoning at a more abstract layer versus the development of meta-theory to transfer the verification results between the layers. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87873-5_18 | VSTTE |
Keywords | Field | DocType |
reasoning step,application layer,overall system correctness,verification result,pervasive formal verification,verisoft approach,systems verification,various abstraction level,abstract layer,system level software,different layer,abstraction level,formal verification | Application layer,Programming language,Intelligent verification,Computer science,Correctness,Microkernel,Theoretical computer science,Verification,Abstraction layer,High-level verification,Formal verification | Conference |
Volume | ISSN | Citations |
5295 | 0302-9743 | 26 |
PageRank | References | Authors |
4.29 | 20 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eyad Alkassar | 1 | 266 | 22.49 |
| Mark A. Hillebrand | 2 | 200 | 15.17 |
| Dirk Leinenbach | 3 | 534 | 27.36 |
| Norbert W. Schirmer | 4 | 55 | 6.94 |
| Artem Starostin | 5 | 144 | 13.07 |