AMAST Mail - December 1999
[Prev][Next][Index]
SPIN'2000 CFP
=====================================
*** Apologies for multiple copies ***
=====================================
Preliminary Call for Papers and Other Contributions
SPIN'2000
The 7th International SPIN Workshop on
Model Checking of Software
Stanford University
California, USA
August 30-31, September 1
Year 2000
http://ase.arc.nasa.gov/spin2000
Objectives
==========
The SPIN workshop is a forum for researchers interested in the broad
subject of model checking technologies for analysis and verification
of asynchronous concurrent/distributed systems. Within the last couple
of years, a renewed interest in program verification has emerged, and
this year's workshop has a special emphasis on this subject. Several
attempts have recently been made to use SPIN for model checking
various programming languages, amongst them C, and object oriented
languages such as C++ and Java. Even a mainly graphical design
language such as UML raises the issue of program verification since
UML designs can contain code fragments, and can evolve into fully
fledged programs.
This new trend brings new challenges into focus, such as dealing with
object oriented dynamic memory allocation and garbage collection,
program libraries, and, last but not least, an increased state space
to explore. These problems require new approaches, amongst them
perhaps the most challenging being how to deal with really big state
spaces. Techniques to deal with this include for example static
analysis, abstraction, guided search, and intelligent testing
techniques in between complete state space exploration such as model
checking on the one hand, and partial search, such as simulation on
the other.
Submissions (theoretical as well as practical) addressing software
verification are encouraged, but this is absolutely not a requirement.
Contributions do not have to build on SPIN, and can describe similar
or comparable technologies.
Co-located with FMOODS
======================
The workshop takes place in the week before the FMOODS conference:
IFIP TC6/WG6.1 Third International Conference on Formal Methods for
Open Object-Based Distributed Systems, which occurs September 6-8 at the
same place. See: http://www.ics.uci.edu/~fmds2000.
Solicited Contributions
=======================
Papers
------
Papers must describe original work that is not submitted or accepted
for publication elsewhere. Topics of interest include, but are not
limited to, the following:
- Algorithms
- Storage methods
- Temporal logic
- Extensions of model checking languages and tools
- Analysis and verification of software
- Abstraction
- Static analysis
- Guided model checking
- Automated testing
- Relationship between model checking and testing
- Relationship between model checking and other formal methods
- Environment generation
- Modularity, hierarchy, object orientation and refinement
- Methodologies for model checking designs versus programs
- Significant or unusual practical applications of model checking
- Corporate impact and benefits of model checking techniques
- Analyses and comparative studies of model checking tools
- Real-time
Tutorials and short courses
---------------------------
Proposals should consist of an abstract of at least one page, to be
published. Longer papers are allowed.
Tool Demonstrations
-------------------
The workshop will allow presentations of tools as part of the
sessions. Submissions of proposals should consist of a short paper up
to 4 pages which will be published if accepted. As informal
information for the purpose of evaluation it is in addition allowed
that a more detailed description of the tool and its capabilities be
sent. This will not be published, and can hence be rather informal;
for example, an already existing manual.
Invited Speakers:
=================
A collection of invited speakers will give presentations. These are still to
be announced.
Important Dates
===============
May 1, 2000 : Deadline for submission of contributions
June 5, 2000 : Notification of acceptance
June 26, 2000 : Camera-ready copy (postscript) for proceedings due
Submissions and Publication
===========================
Papers, no longer than 20 pages, can be submitted by email in
postscript format to:
havelund@ptolemy.arc.nasa.gov
It is intended to publish selected papers, edited tutorial materials
and tool descriptions as proceedings in a volume of Springer-Verlag's
Lecture Notes in Computer Science series. Therefore final camera-ready
copies (and not necessarily first submissions) will be required in
LNCS format, see http://www.springer.de/comp/lncs/Authors.html.
Workshop Organization
=====================
Klaus Havelund (NASA Ames Research Center,RECOM) havelund@ptolemy.arc.nasa.gov
Gerard Holzmann (Bell Labs) gerard@research.bell-labs.com
John Penix (NASA Ames Research Center) jpenix@ptolemy.arc.nasa.gov
Willem Visser (NASA Ames Research Center,RIACS) wvisser@ptolemy.arc.nasa.gov
Program Committee
=================
- Dennis Dams (Eindhoven University, Holland)
- David Dill (Stanford University, USA)
- Orna Grumberg (The Technion, Israel)
- John Hatcliff (Kansas State University, USA)
- Bengt Jonsson (Uppsala University, Sweden)
- Kim Larsen (Aalborg University, Denmark)
- Stefan Leue (University of Waterloo, Canada)
- Doron Peled (Bell Labs/CMU, USA)
- Natarajan Shankar (SRI, USA)
- Moshe Y. Vardi (Rice University, USA)
- Pierre Wolper (Universite de Liege, Belgium)
Electronic Information
======================
Workshop email address : havelund@ptolemy.arc.nasa.gov
Workshop homepage : http://ase.arc.nasa.gov/spin2000
NASA Ames homepage : http://ase.arc.nasa.gov
SPIN homepage : http://netlib.bell-labs.com/netlib/spin/whatispin.html
(includes information about previous workshops)
[
AMAST Mail - December 1999
|
November 1999 |
January 2000 |
Latest Update |
AMAST Mail Meta-Index |
AMAST Mail 1999 |
AMAST
]