Overview

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 (such as BDDs), experimental results in industrial settings, bounded model checking of infinite systems, translation schemes, and SAT techniques for BMC.

Program

• BMC program
• BMC accepted papers
• BMC pre-proceedings

Invited Talks

• Tuesday, August 15th, 10:30‑11:30
  Ilkka Niemela
  Bounded Model Checking, Answer Set Programming, and Fixed Points [pdf]
• Tuesday, August 15th, 14:00‑15:00
  Fabio Somenzi
  Techniques for proving properties with SAT-based MC [pdf]

Organization

The workshop will be organized in the same way as in previous years. In particular there will be workshop proceedings. Extended versions of the 2003 workshop appeared in a special issue of the journal STTT dedicated to BMC'03. A special issue for BMC'04-BMC'05 will appear in FMSD. We will likewise do the same for BMC'06, if the quality of the papers is appropriate.

Chairs

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

Program Committee

Per Bjesse (Synopsys, USA)

Alessandro Cimatti (IRST,Italy)

Raanan Fraer (Intel, Israel)

Danny Geist (Intel, Israel)

Aarti Gupta (NEC, USA)

Alan Hu (Univ. of British Columbia, Canada)

Koen Claessen (Chalmers University of Technology)

Daniel Kroening (ETH-Zurich, Switzerland)

Ken McMillan (Cadence, USA)

Ofer Strichman (Technion, Israel), Co-chair

Yunshan Zhu (Consultant, USA)

Old Web Page