Bounded Model Checking of Blackbox Designs via Quantified Boolean Formulas

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.

Weitere Informationen: http://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=44

Projektbeginn: 2000
Projektende: (unbegrenzt)

Becker B

Albert-Ludwigs-Universität Freiburg
Rechnerarchitektur
Prof. Dr. Bernd Becker
Georges-Köhler-Allee 051
79110 Freiburg i. Br.

Telefon: 0761 203 8140
Fax: 0761 203 8142
http://ira.informatik.uni-freiburg.de

• Miller
• Lewis
• Herbstritt