From   Wed Apr 13 23:31:20 2005
X-Original-To: 
Delivered-To: 
Date: Wed, 13 Apr 2005 13:31:17 -0700 (PDT)
From: Willem Visser 
To: 
Subject: SoftMC'05: Call for Papers
X-Spam-Checker-Version: SpamAssassin 2.64-cstutfi (2004-01-11) on 
	mail.cs.tut.fi
X-Spam-Level: 
X-Spam-Status: No, hits=0.0 required=5.0 tests=none autolearn=no 
	version=2.64-cstutfi
Content-Length: 4298

========================    Call for Papers    ========================


             SoftMC 2005: Workshop on Software Model Checking 

                  http://www.cse.ogi.edu/~byron/SoftMC05

           July 11, 2005 in Edinburgh, Scotland, Just after CAV 

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.

The 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 programs.  Other 
automated verification techniques (e.g., based on static analysis or theorem 
proving) with the same goals are also of interest.  Theoretical results and 
case studies are equally welcome.

Approaches 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:

* Model checking for languages with features such as recursion, references,
  dynamic memory allocation, or object-oriented constructs.

* Static analysis and state-space reductions: slicing, partial-order
  reductions, symmetry reductions, etc.

* Abstraction for software model checking.

* Proving liveness properties

* Symbolic reasoning with accurate program semantics (pointers, bitvector
  arithmetic, etc)

* Applications of model checking to software verification/debugging.

* Advanced testing approaches, e.g., test-case generation via model checking.

* Heuristic search for model checking

* Specifications, e.g., specification patterns, specification mining.


Important dates
~~~~~~~~~~~~~
Submission deadline (FIRM!)          : May 19, 2005 
Notification of acceptance/rejection : June 8, 2005 
Final version due                    : June 13, 2005 
Workshop                             : July 11, 2005 

The body of each submission should not exceed 10 pages, including 
bibliography. The submission may include, in addition, an appendix 
containing technical details, which reviewers may read or not, at 
their discretion.  The manuscript should describe original research 
and contain sufficient detail to assess the merits and relevance of 
the contribution.  Simultaneous submission to other meetings with 
published proceedings and submission of material that has been 
published elsewhere are prohibited.

Submission messages should include the following information in plain
text: names and affiliations of all authors, the title of the paper, 
the contact author's postal and e-mail addresses and phone number, and 
a one- or two-paragraph abstract.  Manuscripts should be in PDF 
(preferred) or PostScript format.

Please submit papers via e-mail to  

The workshop proceedings will be published through Electronic Notes in 
Theoretical Computer Science (ENTCS).

For more information, see the SoftMC 2005: Workshop on Software Model 
Checking website at http://www.cse.ogi.edu/~byron/SoftMC05  .



Program Committee
~~~~~~~~~~~~~~~

Tevfik Bultan, University of California, Santa Barbara 

Byron Cook (Co-organizer), Microsoft Research 

Hubert Garavel, INRIA Rhone-Alpes 

John Hatcliff, Kansas State University

Daniel Kroening, Eidgenossiche Technische Hochschule (ETH), Zurich

Andreas Podelski, Max-Planck-Institut fur Informatik, Saarbrucken 

Scott Stoller (Co-organizer), State University of New York at Stony Brook

Willem Visser (Co-organizer), RIACS/NASA Ames Research Center