16. SPIN 2009: Grenoble, France

Invited Contributions

• Patrice Godefroid:
  Software Model Checking Improving Security of a Billion Computers. 1
  
• Marta Z. Kwiatkowska:
  On Quantitative Software Verification. 2-3
  
• Joseph Sifakis:
  The Quest for Correctness-Beyond a Posteriori Verification. 4
  
• Willem Visser:
  Who Really Cares If the Program Crashes?. 5
  

Regular Papers

• Mordechai Ben-Ari:
  Tool Presentation: Teaching Concurrency and Model Checking. 6-11
  
• Peter C. Dillinger, Panagiotis Manolios:
  Fast, All-Purpose State Storage. 12-31
  
• Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski:
  Efficient Probabilistic Model Checking on General Purpose Graphics Processors. 32-49
  
• David Faragó, Peter H. Schmitt:
  Improving Non-Progress Cycle Checks. 50-67
  
• Malay K. Ganai, Sudipta Kundu:
  Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions. 68-87
  
• Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang:
  Probabilistic Reachability for Parametric Markov Models. 88-106
  
• Alexander Heußner, Tristan Le Gall, Grégoire Sutre:
  Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems. 107-124
  
• Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps:
  A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks. 125-142
  
• Tim Kovse, Bostjan Vlaovic, Aleksander Vreze, Zmago Brezocnik:
  Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation. 143-147
  
• Junghee Lim, Akash Lal, Thomas W. Reps:
  Symbolic Analysis via Semantic Reinterpretation. 148-168
  
• Radek Pelánek, Václav Rosecký:
  EMMA: Explicit Model Checking Manager (Tool Presentation). 169-173
  
• Neha Rungta, Eric G. Mercer, Willem Visser:
  Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. 174-191
  
• Andrey Rybalchenko, Rishabh Singh:
  Subsumer-First: Steering Symbolic Reachability Analysis. 192-204
  
• Sebastian Schmerl, Michael Vogel, Hartmut König:
  Identifying Modeling Errors in Signatures by Model Checking. 205-222
  
• Oliver Sharma, Jonathan Lewis, Alice Miller, Alan Dearle, Dharini Balasubramaniam, Ronald Morrison, Joe Sventek:
  Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin. 223-240
  
• Hubert Garavel, Damien Thivolle:
  Verification of GALS Systems by Combining Synchronous Languages and Process Calculi. 241-260
  
• Martin T. Vechev, Eran Yahav, Greta Yorsh:
  Experience with Model Checking Linearizability. 261-278
  
• Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang:
  Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. 279-295