TY - GEN
T1 - Verifying object-oriented programs with higher-order separation logic in Coq
AU - Bengtson, Jesper
AU - Jensen, Jonas Braband
AU - Sieczkowski, Filip
AU - Birkedal, Lars
PY - 2011
Y1 - 2011
N2 - We present a shallow Coq embedding of a higher-order separation logic with nested triples for an object-oriented programming language. Moreover, we develop novel specification and proof patterns for reasoning in higher-order separation logic with nested triples about programs that use interfaces and interface inheritance. In particular, we show how to use the higher-order features of the Coq formalisation to specify and reason modularly about programs that (1) depend on some unknown code satisfying a specification or that (2) return objects conforming to a certain specification. All of our results have been formally verified in the interactive theorem prover Coq.
AB - We present a shallow Coq embedding of a higher-order separation logic with nested triples for an object-oriented programming language. Moreover, we develop novel specification and proof patterns for reasoning in higher-order separation logic with nested triples about programs that use interfaces and interface inheritance. In particular, we show how to use the higher-order features of the Coq formalisation to specify and reason modularly about programs that (1) depend on some unknown code satisfying a specification or that (2) return objects conforming to a certain specification. All of our results have been formally verified in the interactive theorem prover Coq.
U2 - 10.1007/978-3-642-22863-6_5
DO - 10.1007/978-3-642-22863-6_5
M3 - Conference article
SN - 0302-9743
VL - 6898
SP - 22
EP - 38
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
ER -