Projects per year
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 | |
Publication status | Published - 2011 |
Keywords
- Higher-order separation logic
- Nested triples
- Object-oriented programming
- Modular reasoning
- Coq formalisation
Projects
- 1 Finished
-
ToMeSo: Tools and Methods for Scalable Software Verifications
Sestoft, P. (CoI), Birkedal, L. (PI), Mehnert, H. (CoI), Jensen, J. B. (CoI), Bengtson, J. (CoI), Thamsborg, J. J. (CoI), Hartmann Jensen, M. (CoI), Sieczkowski, F. (CoI), Mehnert, H. (CoI) & Svendsen, K. (CoI)
Independent Research Fund Denmark
01/03/2009 → 30/06/2013
Project: Research