Deductive Verification of System Software in the Verisoft XT Project
| dc.contributor.author | Beckert, Bernhard | |
| dc.contributor.author | Moskal, Michał | |
| dc.date.accessioned | 2018-01-08T09:14:12Z | |
| dc.date.available | 2018-01-08T09:14:12Z | |
| dc.date.issued | 2010 | |
| dc.description.abstract | The main goal of the Verisoft XT project is the creation of methods and tools which allow for the pervasive formal verification of integrated computer systems, and the prototypical realization of four concrete industrial application tasks.In this paper, we report on two of Verisoft XT’s sub-projects, where formal verification is applied to real-world system software, namely Microsoft’s Hypervisor and the embedded operating system PikeOS. We describe the deductive verification technology used in Verisoft XT and the tool chain that implements these methods, including the C verifier called VCC and the SMT solver Z3. | |
| dc.identifier.pissn | 1610-1987 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/11127 | |
| dc.publisher | Springer | |
| dc.relation.ispartof | KI - Künstliche Intelligenz: Vol. 24, No. 1 | |
| dc.relation.ispartofseries | KI - Künstliche Intelligenz | |
| dc.title | Deductive Verification of System Software in the Verisoft XT Project | |
| dc.type | Text/Journal Article | |
| gi.citation.endPage | 61 | |
| gi.citation.startPage | 57 |