Transition power abstractions for deep counterexample detection

DOI10.1007/978-3-030-99524-9_29MaRDI QIDQ6535576zbMATH OpenFDO

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

Publication date 23 January 2024

Copyright license Creative Commons Attribution 4.0 International

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)

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

Cites work

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

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)