BMC'05

Home

Scope

Program

Proceedings

Organization

Call for Papers

Background

Since its introduction in 1999 by Biere, Cimatti, Clarke and Zhu, 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 (such as BDDs), experimental results in industrial settings, bounded model checking of infinite systems, translation schemes, and SAT techniques for BMC.