High-level Proofs about Low-level Programs
Holger Gast, Julia Trieflinger · Technische Universität Berlin – Universitätsbibliothek · 2009
Functional verification of low-level code requires abstractions over the memory model to be effective, since the number of side-conditions induced by byte- addressed memory is prohibitive even with modern automated reasoners. We pro- pose a flexible solution to this challenge: assertions contain explicit memory layouts which carry the necessary side-conditions as invariants. The memory-related proof obligations arising during verification can then be solved using specialized auto- matic proof procedures. The remaining verification conditions about the content of data structures directly reflect a developer's understanding. The development is formalized in Isabelle/HOL.