Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics
Ralf Sasse and Jose Meseguer
Java+ITP is an experimental tool for the verification of properties of
a sequential imperative subset of the Java language. It is based on
an algebraic continuation passing style (CPS) semantics of this
fragment as an equational theory in Maude. It supports compositional
reasoning in a Hoare logic for this Java fragment that we propose and
prove correct with respect to the algebraic semantics. After being
decomposed, Hoare triples are translated into semantically equivalent
first-order verification conditions (VCs) which are then sent to Maude's
Inductive Theorem Prover (ITP) to be discharged. The long-term goal
of this project is to use extensible and modular rewriting logic
semantics of programming languages, for which CPS axiomatizations are
indeed very useful, to develop similarly extensible and modular Hoare
logics on which generic program verification tools can be
based.