Skip to main content

Abstraction and Subsumption in Modular Verification of C Programs

Author(s): Beringer, Lennart; Appel, Andrew W

To refer to this page use:
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 Open image in new window of 𝜓 , that is 𝜙<:𝜓 , then 𝑥:𝜙 implies 𝑥:𝜓 , 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.
Publication Date: 2019
Citation: Beringer, Lennart, and Andrew W. Appel. "Abstraction and Subsumption in Modular Verification of C Programs." In International Symposium on Formal Methods (2019): pp. 573-590. doi:10.1007/978-3-030-30942-8_34
DOI: 10.1007/978-3-030-30942-8_34
ISSN: 0302-9743
Pages: 573 - 590
Type of Material: Conference Article
Series/Report no.: Lecture Notes in Computer Science;
Journal/Proceeding Title: International Symposium on Formal Methods
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.