Speaker: Christoph Gladisch, KIT

Title: On Verifying Relational Specifications of Java Programs with JKelloy

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.  In this talk I will describe 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.