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.
Publications
- JKelloy: A Proof Assistant for Relational Specifications of Java Programs, Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri, In 6th NASA Formal Methods Symposium (NFM), 2014.
- On Verifying Relational Specifications of Java Programs with JKelloy, Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri, Karlsruhe Institute of Technology, Karlsruhe Reports in Informatics, 2014-3, 2014.
- A Proof Assistant for Alloy Specifications, Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri, In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012.
- On Proving Alloy Specifications using KeY, Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri, Karlsruhe Institute of Technology, Technical report 2011-37, 2011.
People
- Aboubakr Achraf El Ghazi
- Mana Taghdiri
- Mattias Ulbrich
- Christoph Gladisch
- Shmuel Tyszberowicz
Tool
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.