Counterexamples revisited: principles, algorithms, applications

DOI10.1007/B12001MaRDI QIDQ5305642zbMATH OpenOpenAlexFDO

Authors Helmut Veith, Edmund Clarke

Publication date 23 March 2010

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

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

Mathematics Subject Classification ID

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

Recommendations

• Fundamental Approaches to Software Engineering
• Counterexamples in Probabilistic Model Checking
• Counterexample generation for discrete-time Markov models: an introductory survey
• Counterexample-guided abstraction refinement for symbolic model checking
• Counterexample classification

Cited in

(21)

• Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
• Generation of minimum tree-like witnesses for existential CTL
• On the Notion of Vacuous Truth
• Producing Short Counterexamples Using “Crucial Events”
• CTL Model-Checking with Graded Quantifiers
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• scientific article; zbMATH DE number 4066342 (Why is no real title available?)
• Minimal counterexamples for linear-time probabilistic verification
• scientific article; zbMATH DE number 2038762 (Why is no real title available?)
• scientific article; zbMATH DE number 1765705 (Why is no real title available?)
• DSValidator: an automated counterexample reproducibility tool for digital systems
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Compositional safety refutation techniques
• Counterexample generation for discrete-time Markov models: an introductory survey
• Fundamental Approaches to Software Engineering
• Diagnostic Information for Realizability
• Finding Counter Examples in Induction Proofs
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• An Efficient Algorithm Finds Noticeable Trends and Examples Concerning the Černy Conjecture
• Counterexample classification
• Transition power abstractions for deep counterexample detection

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: Counterexamples revisited: principles, algorithms, applications

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