| |
15th International SPIN
Workshop on
Model Checking of Software
August 10-12, 2008, Los Angeles, USA
Program
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
|