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.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Niklas Eén, Alan Mishchenko, Nina Amla
• Keywords: Abstraction, CORR 2010, Counterexample-based Abstraction, Counterexample-Based Abstraction Niklas, Education