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

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

2010-08-11

arxiv.org/abs/1008.2021v1

Computer Science

Logic in Computer Science

Accepted for FMCAD 2010

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-586504