On Verifying Relational Specifications of Java Programs with JKelloy

Author:
Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri
Place:
Karlsruhe Institute of Technology, Karlsruhe Reports in Informatics, 2014-3, 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 proved 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.

links

[pdf]

BibTex

@TechReport{elghazi-ulbrich-gladisch-tyszberowicz-taghdiri-techrep2014, 
    author      = {Aboubakr Achraf {El Ghazi} and Mattias Ulbrich and Christoph Gladisch and Shmuel Tyszberowicz and Mana Taghdiri}, 
    title       = {On Verifying Relational Specifications of {Java} Programs with {JKelloy}},  
    institution = {Karlsruhe Institute of Technology},  
    type        = {Karlsruhe Reports in Informatics},  
    issn        = {2190-4782},  
    number      = {2014-3},  
    year        = {2014}
}