Automated Software Analysis Group

JKelloy: A Proof Assistant for Relational Specifications of Java Programs

  • Author:

    Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri

  • Place:

    6th NASA Formal Methods Symposium (NFM), 2014

  • Abstract

    Alloy is a relational specification language with a built-in transitive closure operator which makes it particularly suitable for writing concise specifications of linked data structures. Several tools support Alloy specifications for Java programs. However, they can only check the validity of those specifications with respect to a bounded domain, and thus, in general, cannot provide correctness proofs. This paper presents JKelloy, a tool for deductive verification of Java programs with Alloy specifications. It includes automatically-generated coupling axioms that bridge between specifications and Java states, and two sets of calculus rules that (1) generate verification conditions in relational logic and (2) simplify reasoning about them. All rules have been proven correct. To increase automation capabilities, proof strategies are introduced that control the application of those rules. Our experiments on linked lists and binary graphs show the feasibility of the approach.

BibTex

@InProceedings{elghazi-ulbrich-gladisch-Tyszberowicz-taghdiri-nfm2014,
    author    = {Aboubakr Achraf {El Ghazi} and Mattias Ulbrich and Christoph Gladisch and Shmuel Tyszberowicz and Mana Taghdiri},
    title     = {JKelloy: A Proof Assistant for Relational Specifications of Java Programs},
    booktitle = {6th NASA Formal Methods Symposium (NFM), 2014},
    pages     = {173-187},
    year      = {2014},
    month     = {April-May}
}