Workshop on Software Model Checking

July 23, 2001
Paris, France

Schedule | Registration | Invited Speakers | Dates | Co-Chairs | Program Committee

The growing importance of model checking in hardware verification and the difficulty of producing correct software are driving a growing interest in the application of model checking to software. This leads to many challenges of scientific and practical interest, both in core model checking technology and in supporting techniques, such as program analyses and transformations that help automate abstraction of the data state and reduction of the control state.

This workshop covers all aspects of software model checking and supporting techniques, ranging from verification of high-level requirements specifications to model checking of low-level bytecode. Theoretical results and case studies are equally welcome. Techniques that provide limited guarantees or that work for limited classes of properties are also of interest. We especially encourage submissions that deal with general-purpose programming languages or other languages with similar features. Topics of interest include but are not limited to:

The workshop has a dual mission: it aims to introduce people to the field of software model checking and to be a forum for describing new research. Hence, the workshop will consist of invited presentations by leaders in the field and a selection from the submitted papers.

The proceedings appeared as volume 55 number 3 of Electronic Notes in Theoretical Computer Science.

The workshop will be held after CAV'01 in the same location (la Mutualite). CAV'01 follows FMICS'01 and SAS'01.

Generous support provided by RIACS


Workshop Schedule


Registration is open to everyone and can be done through the CAV registration page. If you are not planning to register for CAV, please contact us about workshop-only registration.

Invited Speakers

The invited speakers will describe their leading-edge work in combining the power of static analysis and model checking. This is an important direction for the field of software model checking and is an especially appropriate topic at a workshop co-located with SAS'01 and CAV'01.

Sriram Rajamani, Model Checking, Program Analysis and Theorem Proving: Kitchen Sink?

John Hatcliff, Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software

Submission Information

Submissions should be in PostScript format. The body of each submission should start with a short abstract and should be at most 10 pages long. The submission may include in addition an appendix containing technical details, which reviewers may read or not, at their discretion. The submission should contain the contact author's physical and e-mail addresses and phone number.

Submissions should be sent by email to softmc01 AT csDOTsunysbDOTedu.


Submission deadline: May 15, 2001
Acceptance notification: June 15, 2001
Final version: July 1, 2001


Scott Stoller Willem Visser
Computer Science Dept. Automated Software Engineering group
State University of New York at Stony Brook NASA Ames Research Center

Program Committee

Tom Ball, Microsoft Research
David Dill, Stanford University
Hubert Garavel, INRIA Rhone-Alpes / VASY
Patrice Godefroid, Bell Laboratories, Lucent Technologies
Susanne Graf, Verimag
Gerard Holzmann Bell Laboratories, Lucent Technologies
Scott Stoller, State University of New York at Stony Brook
Willem Visser, NASA Ames Research Center