Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic

DOI10.1007/978-3-540-73770-4_3MaRDI QIDQ5423862zbMATH OpenOpenAlexFDO

Authors Philipp Rümmer, Muhammad Ali Shah

Publication date 31 October 2007

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73770-4_3

zbMATH Keywords

disprovingprogram logicsprogram verificationtesting

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 4101151
• scientific article; zbMATH DE number 1706329
• scientific article; zbMATH DE number 5499373
• scientific article; zbMATH DE number 107898
• scientific article; zbMATH DE number 4088902
• A dynamic logic for unstructured programs with embedded assertions
• A new technique for verifying and correcting logic programs
• Verifying programs in the calculus of inductive constructions
• A deductive proof system for multithreaded Java with exceptions

Cited in

(5)

• How testing helps to diagnose proof failures
• Weakest pre-condition reasoning for Java programs with JML annotations
• Satisfiability solving and model generation for quantified first-order logic formulas
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• KeY: A Formal Method for Object-Oriented Systems

Describes a project that uses

Uses Software

• SIMPLIFY
• QuickCheck
• ESC/Java
• NuSMV
• KeY

This page was built for publication: Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5423862)