Program for SPIN 2005
=====================

*** MONDAY, August 22 ***

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

10AM Break

10:30AM Session 1 -- State Representation and Abstraction
        Session Chair: Willem Visser

    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
    Session Chair: Rupak Majumdar

    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
    Session Chair: Stefan Leue

6PM "Five-Minute-Madness" Session (for work-in-progress, etc.)
    Session 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
    Session Chair: Luca de Alfaro

10AM Break

10:30AM Session 3 -- Dealing with Complex Data
    Session Chair: Cormac Flanagan

    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
       Session Chair: Patrice Godefroid

    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
       Session Chair: Theo Ruys

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
    Session Chair: Pierre Wolper

10AM Break

10:30AM Session 5 -- Checking Temporal Properties
        Session Chair: Gerard Holzmann

    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
       Session Chair: Susanne Graf

    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 and Peter Mehlitz
       Session Chair: Sarfraz Khurshid

6:30PM End of SPIN 2005