Bounded Model Checking of Blackbox Designs via Quantified Boolean Formulas

| project staff | project description |

Bounded Model Checking (BMC) has become a mature verification technology
in the last years and is used throughout the industry. Simultaneously,
SAT-solvers for solving propositional formulas were heavily investigated
such that the next step to go is to tackle the more complex problem of
deciding quantified boolean formulas (QBF) for real-world applications.
The concept of blackbox designs makes use of both BMC and QBF to analyze
partial circuit implementations and thus enables to find errors in a circuit
design, e.g., at an early design stage.

The main goal of this project is to bring together the
research group of Enrico Giunchiglia, who has an excellent expertise
in QBF-solving, and the research group of Bernd Becker, who has
eminent expertise in BMC of blackbox designs as well as thread-based
SAT-solving, by developing and implementing new techniques for BMC of
blackbox designs via QBF.