Java+ITP: A verification tool based on Hoare logic and algebraic semantics. 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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
- Meseguer, José: Twenty years of rewriting logic (2012)
- Roşu, Grigore; Ştefănescu, Andrei: Towards a unified theory of operational and axiomatic semantics (2012)
- Roşu, Grigore; Ştefănescu, Andrei: From hoare logic to matching logic reachability (2012)
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
- Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project (2007)
- Sasse, Ralf; Meseguer, José: Java+ITP: a verification tool based on Hoare logic and algebraic semantics (2007) ioport