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.