Transition power abstractions for deep counterexample detection

DOI10.1007/978-3-030-99524-9_29zbMATH Open1547.68412MaRDI QIDQ6535576FDOQ6535576

Authors: Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina 

Publication date: 23 January 2024

Recommendations

• Infinite-state invariant checking with IC3 and predicate abstraction
• Transition-Based Directed Model Checking
• Counterexamples revisited: principles, algorithms, applications
• Counterexample-guided abstraction refinement for symbolic model checking
• scientific article; zbMATH DE number 1617333

zbMATH Keywords

model checkingtransition systemsCraig interpolationmodel-based projection

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Cites Work

• Interpolant strength
• Interpolation and SAT-based model checking.
• An interpolating theorem prover
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• Accelerating Interpolation-Based Model-Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Transition invariants and transition predicate abstraction for program termination
• Fast acceleration of ultimately periodic relations
• Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings
• SMT-based model checking for recursive programs
• Under-approximating loops in C programs for fast counterexample detection
• Handbook of model checking
• A calculus for modular loop acceleration
• OpenSMT2: an SMT solver for multi-core and cloud computing
• A unifying view on SMT-based software verification
• Title not available (Why is that?)
• Function summarization modulo theories
• Farkas-based tree interpolation
• Decomposing Farkas Interpolants

Cited In (2)

• The \textsc{Golem} Horn solver
• Lockstep composition for unbalanced loops

This page was built for publication: Transition power abstractions for deep counterexample detection

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