%0 Conference Proceedings
%T A Case Study in Formal Verification Using Multiple Explicit Heaps
%+ Formal Methods and Tools (FMT group)
%A Mostowski, Wojciech
%Z Part 2: Session 1: Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 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)
%C Florence, Italy
%Y Dirk Beyer
%Y Michele Boreale
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7892
%P 20-34
%8 2013-06-03
%D 2013
%R 10.1007/978-3-642-38592-6_3
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01515237/document
%2 https://inria.hal.science/hal-01515237/file/978-3-642-38592-6_3_Chapter.pdf
%L hal-01515237
%U https://inria.hal.science/hal-01515237
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-7892