Forwarded message from [havelund@ptolemy.arc.nasa.gov] sent originally on Mon, 20 Dec 1999 18:41:46 +0800 (GMT-8): : ===================================== : *** 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)

-- Wirtschaftsinformatik, FB5, Universitaet GH Essen Gustaf.Neumann@uni-essen.de, neumann@computer.org http://nestroy.wi-inf.uni-essen.de/Neumann.html