Generating error traces from verification-condition counterexamples

DOI10.1016/J.SCICO.2004.05.016MaRDI QIDQ1776586zbMATH OpenOpenAlexWikidataFDO

Authors 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

Theory of software (68N99)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Error-tracing axiomatic semantics for C-kernel
• Error invariants
• Refinement of Trace Abstraction
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Instrumenting a weakest precondition calculus for counterexample generation
• Error-tracing axiomatic semantics for C-kernel
• Error invariants
• Explaining Verification Conditions
• ExplainHoudini: making Houdini inference transparent

Describes a project that uses

Uses Software

• ESC/Java
• SIMPLIFY
• SPIN

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

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