Objective
Shortly after its introduction Bounded Model Checking has been adopted by most relevant companies as a complementary technique to the more traditional BDD based unbounded symbolic model checking. Largely due to the advances in SAT technology in the last few years, Bounded Model Checking became a leading tool in detection of relatively shallow logical errors, outperforming BDD based tools in most of these cases. The large interest in this technology has created a constant stream of new ideas and improvements that make this technique more and more useful. In this workshop we hope to bring together all those people that are interested in this area to share their ideas and report their results.
Scope
The scope of the workshop includes all theoretical and practical aspects of Bounded Model Checking, including, but not limited to, using SAT technology for unbounded model checking, combining BMC with other tools and techniques, experimental results in an industrial setting, BMC of infinite state systems, translation schemes, and dedicated SAT techniques for BMC.