Sciweavers

Share
CORR
2010
Springer

A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction

9 years 2 months ago
A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction
nd Counterexample-Based Abstraction Niklas Een, Alan Mishchenko EECS Department, University of California Berkeley, USA. Nina Amla Cadence Research Laboratroy Berkeley, USA. This paper presents an efficient, combined formulation idely 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 op the abstraction in a bottom-up fashion. It is argued that the new method is simpler conceptually and implementationwise 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.
Niklas Eén, Alan Mishchenko, Nina Amla
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Niklas Eén, Alan Mishchenko, Nina Amla
Comments (0)
books