Accelerating predicate abstraction by minimum unsatisfiable cores extraction

DOI10.1007/978-981-16-1877-2_1MaRDI QIDQ1980482zbMATH OpenOpenAlexFDO

Authors Jian-Min Zhang, Kefan Ma, Tiejun Li

Publication date 8 September 2021

Full work available at URL https://doi.org/10.1007/978-981-16-1877-2_1

zbMATH Keywords

model checkingformal verificationpredicate abstractionBoolean satisfiabilityminimum unsatisfiable core

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Mathematical problems of computer architecture (68M07)

Recommendations

• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Theory and Applications of Satisfiability Testing
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Predicate abstraction with minimum predicates
• Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction

Cites work

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• Algorithms for computing minimal unsatisfiable subsets of constraints
• An approach for extracting a small unsatisfiable core
• Approximate counting of minimal unsatisfiable subsets
• FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Finding a collection of MUSes incrementally
• MUS Extraction Using Clausal Proofs
• On computing the union of MUSes
• Theory and Applications of Satisfiability Testing
• Towards efficient MUS extraction
• Using local search to find MSSes and MUSes

Cited in

(2)

• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• Faster Extraction of High-Level Minimal Unsatisfiable Cores

This page was built for publication: Accelerating predicate abstraction by minimum unsatisfiable cores extraction

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