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

Ralf Sasse | Zendy; José Meseguer | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Ralf Sasse,

José Meseguer

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2007.06.006

Subject(s) - programming language , hoare logic , computer science , axiomatic semantics , algebraic semantics , separation logic , semantics (computer science) , java , rewriting , theoretical computer science , operational semantics , denotational semantics , correctness

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research