Workshop on Software Model Checking

08:00-09:00 Breakfast and Registration
09:00-10:00 Invited Talk

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

10:00-10:30 Break
10:30-12:00 Model-Checking of Programming Languages

Model checking the garbage collection mechanism of SMV
Cindy Eisner

Model checking Erlang programs - abstracting the context-free structure
Frank Huch

Checking Java implementation of a naming architecture using Testera
Sarfraz Khurshid and Darko Marinov

12:00-13:30 Lunch (on your own)
13:30-14:30 Invited Talk

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

14:30-15:30 Model-Checking of Software Modeling Languages 1

Trail-directed model checking
Stefan Edelkamp, Alberto Lluch Lafuente, and Stefan Leue

Model checking UML state machines and collaborations
Timm Schäfer, Alexander Knapp, and Stephan Merz

15:30-16:00 Break
16:00-17:30 Model-Checking of Software Modeling Languages 2

Analyzing the CRF Java memory model with Murphi
Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom

Automated validation of distributed software using the IF environment.
Marius Bozga, Susanne Graf, and Laurent Mounier

Model checking with abstract types
Kirsten Winter

17:30-18:00 Closing reception