SPIN 2008

15th International SPIN Workshop on
Model Checking of Software

August 10-12, 2008, Los Angeles, USA


Sunday August 10

07:00-9:00 Breakfast

08:00-9:00 Registration

09:00-10:00 Invited talk

Shaz Qadeer, Microsoft Research
Context-Bounded Verification of Concurrent Software

10:00-10:30 Break

10:30-12:30 Session 1 : Implementation Verification

Model Checking Abstract Components within Concrete Software Environments
Tonglaga Bao and Michael Jones

Verifying Multi-threaded C Programs with SPIN
Anna Zaks and Rajeev Joshi

Symbolic Context-Bounded Analysis of Multi-threaded Java Programs
Dejvuth Suwimonteerabuth, Javier Esparza and Stefan Schwoon

Efficient Modeling of Concurrent Systems in BMC
Malay Ganai and Aarti Gupta

12:30-14:00 Lunch

14:00-15:00 Invited talk

Yannis Smaragdakis, Univ. Oregon
Combining Static and Dynamic Reasoning for the Discovery of Program Properties

15:00-15:30 Break

15:30-17:00 Session 2 : Applications

Automated Evaluation of Secure Route Discovery in MANET Protocols
Todd Andel and Alec Yasinsac

Formal Verification of a Flash Memory Device Driver - an Experience Report
Moonzoo Kim, Yunja Choi, Yunho Kim and Hotae Kim

Verifying Compiler Based Refinement of Bluespec Specifications using the SPIN Model Checker
Gaurav Singh and Sandeep Shukla

17:00-17:15 Break

17:15-17:45 The Great Debate

17:45-18:15 SPIN business meeting

18:15-19:15 Reception

Monday August 11

07:00-9:00 Breakfast

09:00-10:00 Invited talk

Matthew Dwyer, Univ. Nebraska
Residual Checking of Safety Properties: Prove What You Can and Monitor the Leftovers

10:00-10:30 Break

10:30-12:30 Session 3 : Symbolic Techniques

Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
Radu Mateescu and Emilie Oudot

Symbolic String Verification: An Automata-based Approach
Fang Yu, Tevfik Bultan, Marco Cova and Oscar Ibarra

State Focusing: Lazy Abstraction for the Mu-Calculus
Harald Fecher and Sharon Shoham

Translating ProbMela Specifications Into the PRISM Language
Frank Ciesinski, Christel Baier, Marcus Groesser and David Parker

12:30-14:00 Lunch

14:00-15:00 Invited talk

Wolfram Schulte, Microsoft Research
Using Dynamic Symbolic Execution to Improve Deductive Verification

15:00-15:30 Break

15:30-17:00 Session 4 : Heuristics

Tackling Large Verification Problems With the Swarm Tool
Gerard Holzmann, Rajeev Joshi and Alex Groce

Resource-Aware Verification using Randomized Exploration of Large State Spaces
Abed Nazha, Stavros Tripakis and Jean-Marc Vincent

Efficient Stateful Dynamic Partial Order Reduction
Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan and Robert M. Kirby

18:30 Workshop Dinner at JiRaffe, 502 Santa Monica Blvd., Santa Monica, CA 90401, phone: 310-917-6671; map.

Tuesday August 12

07:00-9:00 Breakfast

09:00-10:00 Invited talk

Daniel Jackson, MIT
Increasing Modelling Confidence with Unsat Core

10:00-10:30 Break

10:30-12:30 Session 5 : Optimizations

Incremental Hashing for Spin
Viet Yen Nguyen and Theo Ruys

Layered Duplicate Detection in External-Memory Model Checking
Peter Lamborn and Eric Hansen

Dynamic Delayed Duplicate Detection for External Memory Model Checking
Sami Evangelista

Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes
Stefan Leue, Alin Stefanescu and Wei Wei

12:30-14:00 Lunch and Steering Committee Meeting

14:00 END