[TYPES] SPIN 2005 Call for Participation

[Patrice Godefroid]

                      SPIN 2005  Call for Participation

    12th International SPIN Workshop on Model Checking of Software
                 August 22-24, 2005, San Francisco, USA
                     (Co-located with CONCUR 2005)

          http://cm.bell-labs.com/cm/cs/what/spin2005/index.html


REGISTRATION IS NOW OPEN! The early registration deadline is July 20th.

SPIN 2005 is a forum for practitioners and researchers interested in
model-checking based techniques for the validation and analysis of
communication protocols and software systems. The workshop will focus
on topics including theoretical and algorithmic foundations and tools
for software model checking, model derivation from code and code
derivation from models, techniques for dealing with large and infinite
state spaces, and applications. The workshop aims to foster
interactions and exchanges of ideas with all related areas in software
engineering.

SPIN 2005 features:

- 3 invited talks by

    Rajeev Alur        (University of Pennsylvania)
    Dawson Engler      (Stanford University)
    David Wagner       (UC Berkeley)

- 3 invited tutorials on

    Spin/Modex         by Gerard Holzmann and Theo Ruys
    BLAST              by Tom Henzinger, Ranjit Jhala and Rupak Majumdar
    Java PathFinder    by Willem Visser

- 15 research presentations and

- 4 tool presentations.


The program of SPIN 2005 is as follows:

*** MONDAY, August 22 ***

9AM Welcome and Invited Talk -- David Wagner  (joint with SecCo)
     Title: Pushdown Model Checking for Security

10AM Break

10:30AM Session 1 -- State Representation and Abstraction

     An Incremental Heap Canonicalization Algorithm,
     Madanlal Musuvathi and David L. Dill

     Memory Efficient State Space Storage in Explicit Software Model 
Checking,
     Sami Evangelista and Jean-Francois Pradat-Peyre

     Counterexample-based Refinement for a Boundedness Test for CFSM 
Languages,
     Stefan Leue and Wei Wei

12PM Lunch

2PM Session 2 -- Dealing with Concurrency

     Symbolic Model Checking for Asynchronous Boolean Programs,
     Byron Cook, Daniel Kroening and Natasha Sharygina

     Improving Spin's Partial Order Reduction for Breadth First Search,
     Dragan Bosnacki and Gerard J. Holzmann

     Sound Transaction-based Reduction without Cycle Detection,
     Vladimir Levin, Robert Palmer, Shaz Qadeer and Sriram K. Rajamani

3:30PM Break

4PM Invited Tutorial -- Effective Bug Hunting with Spin and Modex,
     by Gerard J. Holzmann and Theo C. Ruys

6PM "Five-Minute-Madness" Session (for work-in-progress, etc.)
     Chair: Stefan Leue

     Rules: anybody attending the workshop can stand up and have the
     floor for maximum 5 minutes (strictly enforced). No slides are
     allowed. A sign-up sheet will be circulated by the session chair
     on the first day.

*** TUESDAY, August 23 ***

9AM Invited Talk -- Dawson Engler  (joint with CONCUR)
     Title: Static Analysis versus Model Checking for Bug Finding

10AM Break

10:30AM Session 3 -- Dealing with Complex Data

     Repairing Structurally Complex Data,
     Sarfraz Khurshid, Ivan Garcia and Yuk Lai Suen

     Crafting a Promela Front-End with Abstract Data Types to Mitigate
     the Sensitivity of (Compositional) Analysis to Implementation
     Choices,
     Yung-Pin Cheng

     Behavioural Models for Hierarchical Components,
     Tomas Barros, Ludovic Henrio and Eric Madelaine

12PM End of session

12:30PM Lunch

2:30PM Session 4 -- Tool Presentations

     ETCH: An Enhanced Type Checking Tool for Promela,
     Alastair F. Donaldson and Simon J. Gay

     Enhanced Probabilistic Verification with 3Spin and 3Murphi,
     Peter C. Dillinger and Panagiotis Manolios

     SPLAT: A Tool for Model-Checking and Dynamically-Enforcing 
Abstractions,
     Anil Madhavapeddy, David Scott and Richard Sharp

     Learning-Based Assume-Guarantee Verification,
     Dimitra Giannakopoulou and Corina S. Pasareanu

4PM Break

4:30PM Invited Tutorial -- The BLAST Software Verification System,
        by Tom Henzinger, Ranjit Jhala, Rupak Majumdar

6:30PM Business meeting

7:30PM BANQUET

*** WEDNESDAY, August 24***

9AM Invited Talk -- Rajeev Alur  (joint with CONCUR)
     Title: The Benefits of Exposing Calls and Returns

10AM Break

10:30AM Session 5 -- Checking Temporal Properties

     On-the-fly Emptiness Checks for Generalized Buchi Automata,
     Jean-Michel Couvreur, Alexandre Duret-Lutz and Denis Poitrenaud

     Stuttering Congruence for Chi,
     Bas Luttik and Nikola Trcka

     Verifying Pattern-Generated LTL Formulas: A Case Study,
     Salamah Salamah, Ann Gates, Steve Roach and Oscar Mondragon

12PM End of session

12:30PM Lunch

2:30PM Session 6 -- Checking Security and Real-Time Properties

     Generic Verification of Security Protocols,
     Abdul Sahid Khan, Madhavan Mukund and S. P. Suresh

     Using SPIN and Eclipse for Optimized High-Level Modeling and 
Analysis of Computer Network Attack Models,
     Gerrit Rothmaier, Tobias Kneiphoff and Heiko Krumm

     Model Checking Machine Code with the GNU Debugger,
     Eric Mercer and Michael Jones

4PM Break

4:30PM Invited Tutorial -- Model Checking Programs with Java PathFinder,
        by Willem Visser

6:30PM End of SPIN'2005


Program Chair:
Patrice Godefroid  (Bell Laboratories, Lucent Technologies)

Program Committee:
George Avrunin     (U. Mass. Amherst, USA)
Dennis Dams        (Bell Labs, USA)
Stefan Edelkamp    (U. Dortmund, Germany)
Cormac Flanagan    (UC Santa Cruz, USA)
Jaco Geldenhuys    (Tampere U., Finland)
Patrice Godefroid  (Bell Labs, USA; chair)
Susanne Graf       (Verimag, France)
Gerard Holzmann    (NASA JPL, USA)
Sarfraz Khurshid   (UT Austin, USA)
Stefan Leue        (U. Konstanz, Germany)
Rupak Majumdar     (UCLA, USA)
Laurent Mounier    (Verimag, France)
Shaz Qadeer        (Microsoft, USA)
Theo Ruys          (U. Twente, the Netherlands)
Willem Visser      (NASA Ames, USA)
Pierre Wolper      (U. Liege, Belgium)

Advisory Committee:
Gerard Holzmann    (NASA JPL, USA; chair)
Amir Pnueli        (Weizmann Inst., Israel)

Steering Committee:
Thomas Ball        (Microsoft, USA)
Susanne Graf       (Verimag, France)
Stefan Leue        (U. Konstanz, Germany)
Moshe Vardi        (Rice U., USA)
Pierre Wolper      (U. Liege, Belgium; chair)