Contact

http://ie.technion.ac.il/BMC06
bmc06@ie.technion.ac.il

Invited Speaker

Chairs

Armin Biere, Johannes Kepler University, Linz, Austria
Ofer Strichman, Technion, Haifa, Israel

Program Committee

Important Dates

Objective

Largely due to the advances in SAT technology in the last few years and the development of SAT-based verification technology (rather than only falsification), Bounded Model Checking and its extensions have by now been adopted by most EDA companies interested in formal verification as the leading model checking technique. The large interest in this technology has created a constant stream of new ideas and improvements that make this technique more and more useful and appealing to the industry. 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.

Submission

Submissions are restricted to up to 14 pages in ENTCS style. Please use the LaTeX macros provided for the preliminary proceedings of BMC'06 at http://www.math.tulane.edu/~entcs and do not shrink the margins. (NEW: since entcs has not made special style files for the FLOC workshops yet, use the generic style files instead) For submission send a PDF or Postscript version of your paper to bmc06@ie.technion.ac.il.

Accepted papers will be published electronically through ENTCS at http://www.elsevier.nl/locate/entcs. They will also be published in informal proceedings that will be given to all participants of the workshop. We also consider inviting selected papers to a special Journal issue dedicated to BMC'06, going through an additional reviewing process.