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.|
|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|
|Pages:||573 - 590|
|Type of Material:||Conference Article|
|Series/Report no.:||Lecture Notes in Computer Science;|
|Journal/Proceeding Title:||International Symposium on Formal Methods|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.