On Combining 01X-Logic and QBf

摘要

We discuss how to combine 01X-logic and quantified boolean formulas (QBF) within a homogeneous SAT/QBF-framework in the context of bounded model checking of blackbox designs. The proposed combination allows a flexible handling of blackboxes w.r.t. computational resources. Preliminary results show the scalability of the approach.