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)

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

Describes a project that uses

Uses Software

• ESC/Java
• SPIN
• SIMPLIFY

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)