Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic

DOI10.1007/978-3-540-73770-4_3zbMath1196.68053OpenAlexW1522637266MaRDI QIDQ5423862

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

testingprogram verificationprogram logicsdisproving

Mathematics Subject Classification ID

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

Related Items

KeY: A Formal Method for Object-Oriented Systems ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Could We Have Chosen a Better Loop Invariant or Method Contract?

Uses Software

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

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