High-level Proofs about Low-level Programs - Gast, Holger; Trieflinger, Julia (Electronic Communications of the EASST, 2009)
Functional verification of low-level code requiresabstractions over the memory model to be effective, sincethe number of side-conditions induced by byte-addressedmemory is prohibitive even with modern automated reasoners.We propose a flexible solution to this challenge: assertionscontain explicit memory layouts which carry the necessaryside-conditions as invariants. The memory-related proofobligations arising during verification can then be solvedusing specialized automatic proof procedures. The remainingverification conditions about the content of data structuresdirectly reflect a developer's understanding. The development is formalized in Isabelle/HOL.