Automated Software Analysis Group

JKelloy: A Proof Assistant for Relational Specifications of Java Programs

JKelloy is a tool for deductive verification of Java programs with Alloy -- a declarative first-order relational logic with built-in operators for transitive closure and cardinality -- specifications.

JKelloy automatically generate coupling axioms that bridge between specifications and Java states. It also provides 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, JKelloy provides tailored proof strategies that control the application of calculi rules.





We will be happy to share the tool upon your request. Please feel free to send an email to A. Achraf El Ghazi or Mana Taghdiri.