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.
Type de document :
Communication dans un congrès
Dirk Beyer; Michele Boreale. 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. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.20-34, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_3〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01515237
Contributeur : Hal Ifip <>
Soumis le : jeudi 27 avril 2017 - 10:46:43
Dernière modification le : jeudi 27 avril 2017 - 14:43:59
Document(s) archivé(s) le : vendredi 28 juillet 2017 - 12:32:31

Fichier

978-3-642-38592-6_3_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Wojciech Mostowski. A Case Study in Formal Verification Using Multiple Explicit Heaps. Dirk Beyer; Michele Boreale. 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. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.20-34, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_3〉. 〈hal-01515237〉

Partager

Métriques

Consultations de la notice

533

Téléchargements de fichiers

34