A Case Study in Formal Verification Using Multiple Explicit Heaps - Formal Techniques for Distributed Systems Access content directly
Conference Papers Year : 2013

A Case Study in Formal Verification Using Multiple Explicit Heaps

Wojciech Mostowski
  • Function : Author
  • PersonId : 1007062


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.
Fichier principal
Vignette du fichier
978-3-642-38592-6_3_Chapter.pdf (402.21 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01515237 , version 1 (27-04-2017)





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⟩
1063 View
146 Download



Gmail Facebook X LinkedIn More