A case study in formal verification using multiple explicit heaps

Wojciech Mostowski

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    7 Citations (Scopus)
    5 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationFormal Techniques for Distributed Systems
    Subtitle of host publicationJoint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Florence, Italy, June 3-5, 2013. Proceedings
    EditorsDirk Beyer, Michele Boreale
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages20-34
    Number of pages15
    ISBN (Print)978-3-642-38591-9
    DOIs
    Publication statusPublished - Jun 2013
    EventJoint IFIP 15th WG 6.1 International Conference on Formal Techniques for Distributed Systems, FMOODS/FORTE 2013 - Florence, Italy
    Duration: 3 Jun 20135 Jun 2013
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume7892
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    ConferenceJoint IFIP 15th WG 6.1 International Conference on Formal Techniques for Distributed Systems, FMOODS/FORTE 2013
    Abbreviated titleFMOODS/FORTE
    CountryItaly
    CityFlorence
    Period3/06/135/06/13

    Keywords

    • Automata
    • Concurrency
    • Model checking
    • Polymorphic types
    • Security

    Fingerprint Dive into the research topics of 'A case study in formal verification using multiple explicit heaps'. Together they form a unique fingerprint.

    Cite this