[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

2nd Call for Papers

16th International SPIN Workshop on Model Checking of Software

June 26--28, 2009, Grenoble, France
Co-located with CAV 2009 <http://www-cav2009.imag.fr/>
URL: http://ti.arc.nasa.gov/event/spin09/

 Aim and Scope

The SPIN workshop is a forum for practitioners and researchers
interested in state space-based techniques for the validation and
analysis of software systems. The focus of the workshop is on
theoretical advances and empirical evaluations based on explicit
representations of state spaces, as implemented in the SPIN model
checker or other tools, or techniques based on combinations
of explicit and other symbolic representations. We welcome papers
describing the development and application of state-space and
path-exploration techniques for the testing and the verification of
security-critical software, enterprise and web applications, embedded
software, and other interesting software platforms.
The workshop aims to encourage interactions and exchanges of
ideas with all related areas in software engineering.

 Topics of Interest include (but are not limited to):

* Algorithms and storage methods for explicit-state model checking
* Theoretical and algorithmic foundations of model-checking based analysis
* Directed model checking using heuristics
* Parallel or distributed model checking
* Model checking of timed and probabilistic systems
* Abstraction and symbolic execution techniques in relation to
 software verification
* Static analysis for state space reduction
* Combinations of enumerative and symbolic techniques
* Analysis for modeling languages, such as UML/state charts
* Property specification languages, including new forms of temporal logic
* Model checking for various programming languages and code analysis
* Automated testing using state space and/or path exploration techniques
* Derivation of specifications, test cases, or other useful material 
from state spaces
* Combination of model-checking techniques with other analysis techniques
* Modularity and compositionality
* Comparative studies, including comparisons with other
 model-checking techniques
* Case studies of interesting systems or with interesting results
* Engineering and implementation of model-checking tools and platforms
* Benchmarks for software verification

 Solicited Contributions

We solicit two kinds of papers:

* TECHNICAL PAPERS. These papers should contain original work which
 has not been submitted or accepted for publication elsewhere.
 Submissions should adhere to the LNCS format and should be no
 longer than 18 pages.

* TOOL PAPERS. These papers should describe novel tools or tool
 extensions. If previous versions of the described tool have been
 published before, the novel features of the tool should be
 explained clearly. These papers should also specify availability
 of the tool, number of users, and applications/case studies. Tool
 paper submissions should consist of two parts. The first part is
 at most 5 pages in LNCS format. The name "Tool Presentation"
 should appear in the title. If accepted, this 5 page paper will be
 published in the workshop proceedings. The second part should
 describe an informal plan for the oral presentation of the tool.
 This part will not be included in the proceedings.

If accepted, both regular and tool papers will be presented at the
conference and will be included in the workshop proceedings. At
least one author of each accepted paper is expected to be present
at the conference. Submissions are held confidential until publication.

 Submission and Publication

As in previous years, the proceedings of this edition of the workshop
will appear in Lecture Notes in Computer Science.

 Important Dates

Paper submission: March 9, 2009
Notification of acceptance: April 10, 2009
Final papers due: April 17, 2009
Workshop: June 26-28 Friday -- Sunday, 2009

 Invited Speakers:

Patrice Godefroid, Microsoft Research, USA
Marta Kwiatkowska, Oxford University, UK
Joseph Sifakis (Turing Award 2007), VERIMAG, France
Willem Visser, SEVEN Networks, USA


Program Chair:

Corina Pasareanu, Carnegie Mellon U/NASA Ames, USA

Program Committee:

Christel Baier, U Bonn, Germany
Dragan Bosnacki, Eindhoven U, Netherlands
Patricia Bouyer, √ČNS de Cachan, France
Lubos Brim, Masaryk U, Czech Republic
Marsha Chechik, U Toronto, Canada
Matthew Dwyer, U Nebraska, USA
Stefan Edelkamp, TU Dortmund, Germany
Susanne Graf, VERIMAG, France
Jaco Geldenhuys, U Stellenbosch, South Africa
Klaus Havelund, JPL, USA
Gerard Holzmann, JPL, USA
Radu Iosif, VERIMAG, France
Michael Jones, Brigham Young U, USA
Sarfraz Khurshid, UT Austin, USA
Orna Kupferman, Hebrew U, Israel
Stefan Leue, U Konstanz, Germany
Rupak Majumdar, UC Los Angeles, USA
Madan Musuvathi, Microsoft Research, USA
Koushik Sen, UC Berkeley, USA
Scott Stoller, Stony Brook U, USA
Farn Wang, National Taiwan U, Taiwan
Pierre Wolper, U Liege, Belgium

Steering Committee:

Dragan Bosnacki, Eindhoven U, Netherlands
Stefan Edelkamp, TU Dortmund, Germany
Susanne Graf, VERIMAG, France
Klaus Havelund, JPL, USA
Stefan Leue (chair), U Konstanz, Germany
Rupak Majumdar, UC Los Angeles, USA
Pierre Wolper, U Liege, Belgium

Advisory Committee:

Gerard Holzmann (chair), JPL, USA
Amir Pnueli, New York U, USA
Moshe Vardi, Rice U, USA

Corina Pasareanu, PhD

Reply via email to