Mechanized, compositional verification of low-level code

Abstract

For many safety-critical systems besides functional correctness, termination properties are especially important. Ideally, such properties are not only established for high-level representations of a system, but also for low-level representations. In this paper, we therefore present a compositional semantics and a related proof calculus for possibly non-deterministic low-level languages. The calculus facilitates total correctness proofs about program representations given in a low-level language. We cope with the complexity inherent to such proofs by mechanizing the entire theory using the theorem prover Isabelle/HOL and exploiting the provers mechanisms for constructing well-founded relations. © 2014 Springer International Publishing.