Skip to Main content Skip to Navigation
Conference papers

A Case Study in Formal Verification Using Multiple Explicit Heaps

Abstract : In the context of the KeY program verifier and the associated Dynamic Logic for Java we discuss the first instance of applying a generalised approach to the treatment of memory heaps in verification. Namely, we allow verified programs to simultaneously modify several different, but possibly location sharing, heaps. In this paper we detail this approach using the Java Card atomic transactions mechanism, the modelling of which requires two heaps to be considered simultaneously – the basic and the transaction backup heap. Other scenarios where multiple heaps emerge are verification of real-time Java programs, verification of distributed systems, modelling of multi-core systems, or modelling of permissions in concurrent reasoning that we currently investigate for KeY. On the implementation side, we modified the KeY verifier to provide a general framework for dealing with multiple heaps, and we used that framework to implement the formalisation of Java Card atomic transactions. Commonly, a formal specification language, such as JML, hides the notion of the heap from the user. In our approach the heap becomes a first class parameter (yet transparent in the default verification scenarios) also on the level of specifications.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Thursday, April 27, 2017 - 10:46:43 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Document(s) archivé(s) le : Friday, July 28, 2017 - 12:32:31 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Wojciech Mostowski. A Case Study in Formal Verification Using Multiple Explicit Heaps. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.20-34, ⟨10.1007/978-3-642-38592-6_3⟩. ⟨hal-01515237⟩



Record views


Files downloads