High-level Proofs about Low-level Programs

Holger Gast, Julia Trieflinger

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 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.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.23.319

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.23.319.304

Hosted By Universit├Ątsbibliothek TU Berlin.