Name
Title | ||
|---|---|---|
A single-instance incremental SAT formulation of proof- and counterexample-based abstraction |
Abstract | ||
|---|---|---|
This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, this new method is formulated as a single, incremental SAT-problem, interleaving CBA and PBA to develop the abstraction in a bottom-up fashion. It is argued that the new method is simpler conceptually and implementation-wise than previous approaches. As an added bonus, proof-logging is not required for the PBA part, which allows for a wider set of SAT-solvers to be used. |
Year | Venue | Keywords |
|---|---|---|
2010 | Clinical Orthopaedics and Related Research | added bonus,proof-based abstraction,abstraction method,single-instance incremental sat formulation,new method,previous work,pba part,counterexample-based abstraction,interleaving cba,previous approach,bit-level verification,logic gates,boolean functions,interpolation,formal verification,data structures,sat solver,computability,algorithm design and analysis |
DocType | Volume | Citations |
Conference | abs/1008.2021 | 18 |
PageRank | References | Authors |
1.24 | 9 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Niklas Een | 1 | 1573 | 66.34 |
| Alan Mishchenko | 2 | 982 | 84.79 |
| Nina Amla | 3 | 318 | 16.23 |