High-level Proofs about Low-level Programs

2009/12/17 by Holger Gast, Gast, Holger, Julia Trieflinger +1
Computer Science · #Logic, programming, and type systems #Security and Verification in Computing #Formal Methods in Verification

paper · doi:10.14279/tuj.eceasst.23.319.304

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.

Related

• High-level Proofs about Low-level Programs
• Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
• Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
• Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)
• A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability