Generating error traces from verification-condition counterexamples

DOI10.1016/j.scico.2004.05.016zbMath1075.68018OpenAlexW1989547358WikidataQ124816668 ScholiaQ124816668MaRDI QIDQ1776586

K. Rustan M. Leino, James B. Saxe, Todd D. Millstein

Publication date: 12 May 2005

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2004.05.016

zbMATH Keywords

errors in computer programs

Mathematics Subject Classification ID

Related Items (5)

Instrumenting a weakest precondition calculus for counterexample generation ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ ExplainHoudini: Making Houdini Inference Transparent ⋮ Explaining Verification Conditions

Uses Software

• SPIN
• SIMPLIFY
• ESC/Java

This page was built for publication: Generating error traces from verification-condition counterexamples