Verifying object-oriented programs with higher-order separation logic in Coq

Jesper Bengtson; Jonas Braband Jensen; Filip Sieczkowski; Lars Birkedal

doi:10.1007/978-3-642-22863-6_5

Verifying object-oriented programs with higher-order separation logic in Coq

Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal

Computer Science

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

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.

Original language	English
Book series	Lecture Notes in Computer Science
Volume	6898
Pages (from-to)	22-38
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-642-22863-6_5
Publication status	Published - 2011

Keywords

Higher-order separation logic
Nested triples
Object-oriented programming
Modular reasoning
Coq formalisation

Access to Document

10.1007/978-3-642-22863-6_5

PDFSubmitted manuscript, 360 KB

Cite this

@inproceedings{7ae072867b194d2fab53b1dcc5855410,

title = "Verifying object-oriented programs with higher-order separation logic in Coq",

abstract = "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.",

keywords = "Higher-order separation logic, Nested triples, Object-oriented programming, Modular reasoning, Coq formalisation",

author = "Jesper Bengtson and Jensen, {Jonas Braband} and Filip Sieczkowski and Lars Birkedal",

year = "2011",

doi = "10.1007/978-3-642-22863-6_5",

language = "English",

volume = "6898",

pages = "22--38",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

}

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.

KW - Higher-order separation logic

KW - Nested triples

KW - Object-oriented programming

KW - Modular reasoning

KW - Coq formalisation

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 -