A framework for counterexample generation and exploration

DOI10.1007/978-3-540-31984-9_17MaRDI QIDQ5316437zbMATH OpenOpenAlexFDO

Authors Marsha Chechik, Arie Gurfinkel

Publication date 13 September 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107062

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Debugging of concurrent systems using counterexample analysis
• Counterexamples revisited: principles, algorithms, applications
• What went wrong: Explaining counterexamples
• Making the most of BMC counterexamples
• Understanding counterexamples with \texttt{explain}

Cited in

(14)

• Instrumenting a weakest precondition calculus for counterexample generation
• Producing explanations for rich logics
• Debugging of concurrent systems using counterexample analysis
• Pardinus: a temporal relational model finder
• Making the most of BMC counterexamples
• Counterexample-Guided Model Synthesis
• Explaining counterexamples using causality
• Flaw detection in formal specifications
• DSValidator: an automated counterexample reproducibility tool for digital systems
• Efficient debugging in a formal verification environment
• Understanding counterexamples for relational properties with \textit{DIbugger}
• Counterexamples revisited: principles, algorithms, applications
• FocusCheck: A tool for model checking and debugging sequential C programs
• Explainable online monitoring of metric temporal logic

This page was built for publication: A framework for counterexample generation and exploration

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