Deductive Verification of System Software in the VerisoftXT Project
Bernhard Beckert, Michal Moskal
The main goal of the VerisoftXT 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 VerisoftXT'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 VerisoftXT and
the tool chain that implements these methods, including the Verifying
C Compiler (VCC) and the automatic theorem prover Z3.