SPIN 2009 PROGRAM
Friday, June 26, 2009
8.30 – 9: Opening
9 – 10: Invited Talk
- Willem Visser. Who really cares if the program crashes?
10 – 10.30: Break
10.30 – 12: Symbolic Analysis
- Junghee Lim, Akash Lal and Thomas Reps. Symbolic Analysis via Semantic Reinterpretation
- Andrey Rybalchenko and Rishabh Singh. Subsumer-first: A new Heuristic for Guided Symbolic Reachability Analysis
- Neha Rungta, Eric Mercer and Willem Visser. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution
12 – 14: Lunch
14 – 15: Invited Talk
- Marta Kwiatkowska. On Quantitative Software Verification
15 – 15.30: Break
15.30 – 17: Probabilistic Model Checking and Abstraction Refinement
- Stefan Edelkamp, Damian Sulewski and Dragan Bosnacki. Efficient Probabilistic Model Checking on General Purpose Graphics Processors
- Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang. Probabilistic Reachability for Parametric Markov Models
- Alexander Heußner, Grégoire Sutre and Tristan Le Gall. Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems
Saturday, June 27, 2009
9 – 10: Invited Talk
- Joseph Sifakis. The Quest for Correctness - Beyond a posteriori Verification
10 – 10.30: Break
10.30 – 12: Advances in Software Model Checking
- Peter Dillinger and Panagiotis Manolios. Fast, All-Purpose State Storage
- David Faragó and Peter H. Schmitt. Improving Non-progress Cycle Checks
- Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan and Chao Wang. Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis
12 – 14: Lunch
14 – 15.30: Atomicity and Linearizability
- Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas Reps. A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
- Malay Ganai and Sudipta Kundu. Reduction of Verification Conditions for Concurrent System using Mutually Atomic Transactions
- Martin Vechev, Eran Yahav and Greta Yorsh. Experience with Checking Linearizability
15.30 – 16: Break
16 – 17.30: Tool Presentations
- Radek Pelanek and Václav Rosecký. EMMA: Explicit Model Checking Manager
- Tim Kovse, Bostjan Vlaovic, Aleksander Vreze and Zmago Brezocnik. Eclipse Plug-in for Spin and st2msc Tools
- Mordechai (Moti) Ben-Ari. Tool Presentation: Teaching Concurrency and Model Checking
19.30: Workshop Dinner: Overlooking Grenoble "La Bastille"
Sunday, June 28, 2009
9 – 10: Invited Talk
- Patrice Godefroid. Software Model Checking Improving Security of a Billion Computers
10 – 10.30: Break
10.30 – 12: Applications
- Damien Thivolle and Hubert Garavel. Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
- Sebastian Schmerl, Michael Vogel and Hartmut König. Identifying Modeling Errors in Signatures by Model Checking
- Oliver Sharma, Jonathan Lewis, Alice Miller, Al Dearle, Dharini Balasubramaniam, Ron Morrison and Joe Sventek. Towards Verifying Correctness of Wireless Sensor Network Applications using Insense and Spin
12: Closing
- NASA Official: Dave Korsmeyer
- Curator: ASANI Solutions