Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings (Lecture Notes in Computer Science, 5578)

Invited Contributions.- Software Model Checking Improving Security of a Billion Computers.- On Quantitative Software Verification.- The Quest for Correctness-Beyond a Posteriori Verification.- Who Really Cares If the Program Crashes?.- Regular Papers.- Tool Presentation: Teaching Concurrency and Model Checking.- Fast, All-Purpose State Storage.- Efficient Probabilistic Model Checking on General Purpose Graphics Processors.- Improving Non-Progress Cycle Checks.- Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions.- Probabilistic Reachability for Parametric Markov Models.- Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems.- A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks.- Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation.- Symbolic Analysis via Semantic Reinterpretation.- EMMA: Explicit Model Checking Manager (Tool Presentation).- Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution.- Subsumer-First: Steering Symbolic Reachability Analysis.- Identifying Modeling Errors in Signatures by Model Checking.- Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin.- Verification of GALS Systems by Combining Synchronous Languages and Process Calculi.- Experience with Model Checking Linearizability.- Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis.