Abstraction and subsumption in modular verification of C programs

Lennart Beringer, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Abstract

Representation predicates enable data abstraction in separation logic, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of subsumption. We demonstrate function-specification subtyping, analogous to subtyping, with a subsumption rule: if ϕ is a of ψ, that is ϕ< : ψ, then x: ϕ implies x: ψ, meaning that any function satisfying specification ϕ can be used wherever a function satisfying ψ is demanded. We extend previous notions of Hoare-logic sub-specification, which already included parameter adaption, to include framing (necessary for separation logic) and impredicative bifunctors (necessary for higher-order functions, i.e. function pointers). We show intersection specifications, with the expected relation to subtyping. We show how this enables compositional modular verification of the functional correctness of C programs, in Coq, with foundational machine-checked proofs of soundness.

Original languageEnglish (US)
Title of host publicationFormal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
EditorsMaurice H. ter Beek, Annabelle McIver, José N. Oliveira
PublisherSpringer
Pages573-590
Number of pages18
ISBN (Print)9783030309411
DOIs
StatePublished - 2019
Event23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019 - Porto, Portugal
Duration: Oct 7 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11800 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
Country/TerritoryPortugal
CityPorto
Period10/7/1910/11/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Keywords

  • Foundational program verification
  • Separation logics
  • Specification subsumption

Fingerprint

Dive into the research topics of 'Abstraction and subsumption in modular verification of C programs'. Together they form a unique fingerprint.

Cite this