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

Niklas Een, Alan Mishchenko, Nina Amla

This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abs…