<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri","sans-serif";}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal">[Apologies if you receive multiple copies]<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"> *******************************************************<br>
Call for Papers: SPIN 2011<br>
18th Int. SPIN Workshop on Model Checking of Software<br>
July 14-15, Snowbird, Utah, USA<br>
Co-located with CAV 2011<br>
<br>
*******************************************************<br>
<br>
========================================================<br>
<br>
The SPIN Deadline Has Been Extended Until April 15th!<br>
<br>
========================================================<br>
<br>
Aim and Scope: <br>
<br>
------------- <br>
<br>
The SPIN workshop is a forum for practitioners and researchers<br>
interested in state space-based techniques for the validation and<br>
analysis of software systems. Theoretical techniques and empirical<br>
evaluations based on explicit representations of state spaces, as<br>
implemented in the SPIN model checker or other tools, or techniques<br>
based on combination of explicit representations with other<br>
representations, are the focus of this workshop.<br>
<br>
We particularly welcome papers describing the development and<br>
application of state space exploration techniques in testing and<br>
verifying embedded software, security-critical software, enterprise<br>
and web applications, and other interesting software platforms. The<br>
workshop aims to encourage interactions and exchanges of ideas with<br>
all related areas in software engineering.<br>
<br>
Important Dates and Deadlines<br>
-----------------------------<br>
Deadline for submission of full papers: 15 April 2011<br>
Notification of acceptance/rejection: 13 May 2011<br>
Deadline for final version of accepted papers: 3 June 2011<br>
Workshop: July 14-15<br>
<br>
<br>
Topics of Interest<br>
------------------<br>
- Algorithms and storage methods for explicit state model checking<br>
- Automated testing using model checking techniques<br>
- Derivation of invariants, test cases, or other useful information<br>
from state spaces<br>
- Abstraction and the use of static analysis to reduce state spaces<br>
- Model checking of programming languages and code analysis<br>
- Directed model checking using heuristics<br>
- Parallel or distributed model checking using multi-core or multiple<br>
computers<br>
- Techniques for dealing with infinite state spaces<br>
- Model checking of timed and probabilistic systems<br>
- Combinations of enumerative and symbolic techniques<br>
- Analysis for modeling languages, including SE languages (UML,...)<br>
- New property specification languages, including new forms of<br>
temporal logic<br>
- Combination of model-checking techniques with other analysis<br>
techniques<br>
- Modularity and compositionnality<br>
- Comparative studies, including to other model checking techniques<br>
- Case studies of interesting systems or with interesting results<br>
- Theoretical and algorithmic foundations of model-checking based<br>
analysis<br>
- Engineering and implementation of model-checking tools and platforms<br>
- Insightful surveys or historical accounts on topics of relevance to<br>
SPIN workshops<br>
<br>
Solicited Contributions<br>
<br>
-----------------------<br>
<br>
With the exception of survey and history papers, the papers should<br>
contain original work which has not been submitted or accepted for<br>
publication elsewhere. Submissions should adhere to the LNCS<br>
format. We solicit two kinds of papers: 1. Technical Papers. No<br>
longer than 18 pages in LNCS format. All accepted technical papers<br>
will be included in the proceedings. 2. Tool Presentations. This kind<br>
of submission should consist of two parts: the first part is at most a<br>
5 page description of the tool. If accepted, this part will be<br>
published in the workshop proceedings. The second part should describe<br>
an informal plan for an oral presentation of the tool. This part will<br>
not be included in the proceedings.<br>
<br>
The proceedings of SPIN usually appear in Springer's Lecture Notes in<br>
Computer Science series. We are confident we will continue this tradition<br>
for the 2011 edition.<br>
<br>
<br>
Organization<br>
------------<br>
Program Chairs:<br>
Alex Groce (Oregon State University, Corvallis)<br>
Madanlal Musuvathi (Microsoft Research, Redmond)<br>
<br>
Program Committee:<br>
James Andrews (University of Western Ontario, London, Canada)<br>
Dragan Bosnacki (Eindhoven University of Technology)<br>
Sebastian Burckhardt (Microsoft Research, Redmond)<br>
Cristian Cadar (Imperial College, London)<br>
George Candea (EPFL, Switzerland)<br>
Sagar Chaki (Software Engineering Institute, Pittsburgh)<br>
Supratik Chakraborty (I.I.T. Bombay, India)<br>
Azadeh Farzan (University of Toronto, Canada)<br>
Susanne Graf (Verimag)<br>
Aarti Gupta (NEC Labs, USA)<br>
Klaus Havelund (Jet Propulsion Laboratory, Pasadena)<br>
Gerard Holzmann (Jet Propulsion Laboratory, Pasadena)<br>
Gerwin Klein (NICTA, Sydney)<br>
Akash Lal (Microsoft Research, India)<br>
Alberto Lluch Lafuente (IMT Institute for Advanced Studies, Lucca)<br>
Rupak Majumdar (Max Planck Institute for Software Systems)<br>
Darko Marinov (University of Illinois, Urbana-Champaign)<br>
David Parker (University of Oxford)<br>
Corina Pasareanu (Carnegie Mellon University/NASA Ames)<br>
Doron Peled (Bar Ilan University)<br>
Koushik Sen (University of California, Berkeley)<br>
Scott Stoller (Stony Brook University)<br>
Murali Talupur (SCL, Intel) <br>
<br>
<o:p></o:p></p>
</div>
</body>
</html>