BMC'03
First International Workshop
on
Bounded Model Checking
13 July, 2003
Boulder, Colorado, USA
Affiliated with CAV'03
(NEW – proceedings and some
presentations are now available from this page)
OBJECTIVES
The objective of BMC'03 is to bring together scientists from academia and industry to report and debate advances in Bounded Model Checking and related issues.
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.
The scope of the workshop includes all theoretical and practical aspects of Bounded Model Checking, including, but not limited to:
1. Combining BMC with other tools and techniques (such as BDD’s)
2. Experimental results in industrial settings
3. Bounded model checking of infinite systems
4. Translation schemes
5. SAT techniques related to BMC
INVITED SPEAKER
(Note the change of invited speaker)
Ken McMillan
Title: From bounded to unbounded model checking
Here is the planned Program, including links to abstracts, and some of the power-point presentations.
The accepted papers will be published in proceedings that will be given to all participants of the workshop. The articles will also be published in issue 4, Volume 89 of ENTCS (Electronic Notes in Theoretical Computer Science), which is devoted to workshops affiliated with CAV.
NEW: This file contains the proceedings (in pdf).
Submissions: May 7, 2003
Notification: June 9, 2003
Final papers: June 16, 2003
Workshop: July 13, 2003
PROGRAM COMMITTEE
David Basin (Freiburg Univ., Germany)
Armin Biere (ETH-Zurich, Switzerland) Co-chair
Per Bjesse (Synopsys, USA)
Alessandro Cimatti (IRST, Italy)
Raanan Fraer (Intel, Israel)
Danny Geist (IBM – HRL, Israel)
Alan Hu (Univ. of British Columbia, Canada)
James Kukula (Synopsys, USA)
Ken McMillan (Cadence, USA)
Sharad Malik (Princeton Univ., USA)
Mary Sheeran (Chalmers Univ. of Technology, Sweden)
Joao M. Silva (Technical Univ. of Lisbon, Portugal)
Ofer Strichman (Carnegie-Mellon
Univ., USA) Co-chair
Toby Walsh (Univ.of York, UK)
Yunshan Zhu (Synopsys, USA)
ORGANIZERS
Please send all inquiries to bmc03@cs.cmu.edu