The Software Model Checking Workshop has met two times in the past: CAV 2001 in Paris, and CAV 2003 in Boulder, Colorado. A great deal of progress has been made since our last meeting. Researchers have continued to develop their own ideas and borrow others from areas such as SAT-solving, decision procedures, and abstract interpretation. The applications have become more impressive. Companies are beginning to develop products based on this research.

What are the new ideas? What are the future trends? What are the current limitations of software model checking? These will be some of the themes at the 2005 Workshop on Software Model Checking, which will provide a forum for researchers and developers to communicate their ideas, ask questions, and learn about new approaches.

Title: Abstraction-refinement for software model checking: What is new?

Abstract: Over the past few years, software model checking based on iterative abstraction refinement schemes have become popular. Several systems (for example SLAM, BLAST, MAGIC) have implemented this scheme. These systems have three basic steps: (1) abstraction, (2) model checking, and (3) refinement. In this talk, I will survey recent advances in each of these steps.

Title: Software Model Checking of Heap Intensive Programs

Abstract: Proving properties of programs manipulating heap allocated storage is challenging. The state space of these programs is infinite. The programs can mutate the heap using destructive pointer updates, creating shared and cyclic structures. Concurrency introduces another challenge as the data and the control of the program interacts in an intricate way.

In the first part I will describe our experience in developing abstractions and abstract interpretation which automatically prove properties of programs manipulating heap allocated storage. The main idea to summarize dynamically allocated storage and pointers by only tracking the "shape" of the heap and use these summarizations for proving properties. These methods can automatically prove properties' ranging from the absence of null dereferences and memory leaks to partial and total correctness. Our current algorithms have very few false alarms but are rather expensive. I will also sketch several methods that may be used to scale these algorithms to larger programs.

A paper describes the first part of the work is available from http://www.cs.tau.ac.il/~msagiv/toplas02.pdf.

SoftMC will be held at Appleton Tower Lecture Theatres in George Square at the University of Edinburgh.

Appleton Tower (AT) is highlighted in the following map. Registration will be held in the Appleton Tower concourse (through the main entrance). It is accessible from Crichton Street opposite the big car park. There is a wide concourse at ground level giving access to lecture theatres 1, 2 and 3, which are entered at the back. On the first floor, there is a wide balcony giving access to lecture theatres 4 and 5. There is a bank of three lifts at the back of the concourse. Toilets can be found on the left-hand side of the concourse.

• Steven P. Reiss
  Checking Component Specifications in Java Systems
• Morgan Magnin, Didier Lime and Olivier (H.) Roux
  An efficient method for computing exact state space of Petri nets with stopwatches
• Bernd Westphal
  LSC Verification for UML Models with Unbounded Creation and Destruction
• A. Armando, M. Benerecetti, J. Mantovani
  Model Checking Linear Programs with Arrays
• Graham Hughes, Sreeranga P. Rajan, Tom Sidle and Keith Swenson
  Error Detection in Concurrent Java Programs
• Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, and Robert M. Kirby
  Gauss: A Framework for Verifying Scientific Computing Software
• Wolfgang Grieskamp, Nikolai Tillmann, and Wolfram Schulte
  XRT -- Exploring Runtime for .NET -- Architecture and Applications
• R. Grosu, X. Huang, S. Jain, S.A. Smolka
  Open-Source Model Checking

Please register via the CAV registration page. Please make your accommodation arrangements soon as it is now very scarce due to the G8 summit demonstrations.