Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics

Ralf Sasse, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)29-46
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number4
DOIs
StatePublished - Jul 28 2007

Keywords

  • Hoare logic
  • Java
  • algebraic semantics
  • program verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics'. Together they form a unique fingerprint.

Cite this