High-level Proofs about Low-level Programs

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 propose 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 automatic 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