Proof-Guided Underapproximation Widening for Bounded Model Checking

DOI10.1007/978-3-031-13185-1_15MaRDI QIDQ6487321zbMATH OpenFDO

Authors Akash Lal, Subhajit Roy

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13185-1_15

Mathematics Subject Classification ID

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

Recommendations

• Computer Aided Verification
• Computing over-approximations with bounded model checking
• PBMC: Symbolic Slicing for the Verification of Concurrent Programs
• Concurrent program verification with invariant-guided underapproximation
• Efficient strategies for CEGAR-based model checking

Cites work

• Back to the future, revisiting precise program verification using SMT solvers
• Concurrent program verification with invariant-guided underapproximation
• Deciding Bit-Vector Arithmetic with Abstraction
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Proof-guided underapproximation-widening for multi-process systems
• Reachability modulo theories

Cited in

(5)

• Efficient strategies for CEGAR-based model checking
• Concurrent program verification with invariant-guided underapproximation
• Proving safety with trace automata and bounded model checking
• Proof-guided underapproximation-widening for multi-process systems
• Distributed bounded model checking

This page was built for publication: Proof-Guided Underapproximation Widening for Bounded Model Checking

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