ECEASST High-level Proofs about Low-level Programs

Abstract: 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