Published as: Lecture Notes in Computer Science, Volume 2648, Springer Verlag, May 2003
| Invited Talk |
Russel, Frege and
Spin... Gerard Holzmann NASA/JPL, Laboratory for Reliable Software | |||||||||||||||||||||||||||||||||||||
| Session
1 SPIN Applications |
Optimal Scheduling using Branch and Bound with
SPIN 4.0
(PDF)
Theo C. Ruys, University of Twente A Requirements Patterns-Driven Approach to Specify Systems and Check Properties (PDF) Sascha Konrad, Michigan State University Laura Campbell, Michigan State University Betty Cheng, Michigan State University Min Deng, Michigan State University Formal Modeling and Analysis of an Avionics Triplex Sensor Voter (PS) Samar Dajani-Brown, Honeywell Darren Cofer, Honeywell Gary Hartmann, Honeywell Steve Pratt, Honeywell | |||||||||||||||||||||||||||||||||||||
| Session
2 Model Checking Algorithms |
Distributed Explicit Fair Cycle
Detection
(PDF)
Ivana Cerna, Faculty of Informatics, Masaryk Universtiy, Brno, Czech Republic Radek Pelanek, Faculty of Informatics, Masaryk Universtiy, Brno, Czech Republic Efficient Model Checking of Safety Properties (PDF) Timo Latvala, Helsinki University of Technology A Light-weight Algorithm for Model Checking with Symmetry Reduction and Weak Fairness (PDF) Dragan Bosnacki, Eindhoven University of Technology, The Netherlands | |||||||||||||||||||||||||||||||||||||
| Session
3 |
A SAT Characterization of Boolean-Program
Correctness
(PDF)
K. Rustan M. Leino, Microsoft Research What Went Wrong: Explaining Counterexamples (PDF) Alex Groce, Carnegie Mellon University Willem Visser, RIACS/NASA Ames Research Center A Nearly Memory-optimal Data Structure for Sets and Mappings (PDF) Jaco Geldenhuys, Institute of Software Systems, Tampere University of Technology Antti Valmari, Institute of Software Systems, Tampere University of Technology | |||||||||||||||||||||||||||||||||||||
| Invited Talk |
Randomized Algorithms for Program Analysis
and Verification George Necula, UC Berkeley | |||||||||||||||||||||||||||||||||||||
| Session
4 Model Checking Applications |
Checking Consistency of SDL+MSC specifications
(PDF)
Deepak D'Souza, Chennai Mathematical Institute Madhavan Mukund, Chennai Mathematical Institute Model Checking Publish-Subscribe Systems (PDF) David Garlan, Carnegie Mellon University S. Khersonsky, Carnegie Mellon University Jung Soo Kim, Carnegie Mellon University A Methodology for Model-checking Ad-hoc Networks (PDF) Irfan Zakiuddin, QinetiQ Michael Goldsmith, Formal Systems (Europe) Ltd. P. Whittaker P. Gardiner | |||||||||||||||||||||||||||||||||||||
| Session
5 Tools |
Unification and Sharing in Timed Automata
Verification
(PDF)
Alexandre David, Uppsala University Gerd Behrmann, Aalborg University Kim Larsen, Aalborg University Wang Yi, Uppsala University The Maude LTL Model Checker and its Implementation (PDF) Steven Eker, SRI Jose Meseguer, University of Illinois at Urbana-Champaign Ambarish Sridharanarayanan, University of Illinois at Urbana-Champaign Software Verification with Blast (PDF) Thomas Henzinger, UC Berkeley Ranjit Jhala, UC Berkeley Rupak Majumdar, UC Berkeley Gregoire Sutre, Labri, France | |||||||||||||||||||||||||||||||||||||
| Session
6 |
Promela Planning
(PDF)
Stefan Edelkamp, Institut fuer Informatik Thread-Modular Model Checking (PDF) Cormac Flanagan, Systems Research Center, HP Labs Shaz Qadeer, Microsoft Research | |||||||||||||||||||||||||||||||||||||
Program Committee | ||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||