Accelerating predicate abstraction by minimum unsatisfiable cores extraction

DOI10.1007/978-981-16-1877-2_1zbMath1481.68032OpenAlexW3153030442MaRDI QIDQ1980482

Kefan Ma, Jianmin Zhang, Tie-Jun Li

Publication date: 8 September 2021

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

zbMATH Keywords

formal verificationmodel checkingBoolean satisfiabilitypredicate abstractionminimum unsatisfiable core

Mathematics Subject Classification ID

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

Cites Work

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

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