TY - GEN
T1 - Abstraction and subsumption in modular verification of C programs
AU - Beringer, Lennart
AU - Appel, Andrew W.
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
KW - Foundational program verification
KW - Separation logics
KW - Specification subsumption
UR - http://www.scopus.com/inward/record.url?scp=85076099692&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076099692&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30942-8_34
DO - 10.1007/978-3-030-30942-8_34
M3 - Conference contribution
AN - SCOPUS:85076099692
SN - 9783030309411
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 573
EP - 590
BT - Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
A2 - ter Beek, Maurice H.
A2 - McIver, Annabelle
A2 - Oliveira, José N.
PB - Springer
T2 - 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
Y2 - 7 October 2019 through 11 October 2019
ER -