12. SPIN 2005: San Francisco, CA, USA

Patrice Godefroid (Ed.): Model Checking Software, 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings. Lecture Notes in Computer Science 3639 Springer 2005, ISBN 3-540-28195-9

Invited Talks/Papers

David Wagner:
Pushdown Model Checking for Security. 1
Cristian Cadar, Dawson R. Engler:
Execution Generated Test Cases: How to Make Systems Code Crash Itself. 2-23

Invited Tutorials

Gerard J. Holzmann, Theo C. Ruys:
Effective Bug Hunting with Spin and Modex. 24-24
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
The BLAST Software Verification System. 25-26
Willem Visser, Peter C. Mehlitz:
Model Checking Programs with Java PathFinder. 27

State Representation and Abstraction

Madanlal Musuvathi, David L. Dill:
An Incremental Heap Canonicalization Algorithm. 28-42
Sami Evangelista, Jean-François Pradat-Peyre:
Memory Efficient State Space Storage in Explicit Software Model Checking. 43-57
Stefan Leue, Wei Wei:
Counterexample-Based Refinement for a Boundedness Test for CFSM Languages. 58-74

Dealing with Concurrency

Byron Cook, Daniel Kroening, Natasha Sharygina:
Symbolic Model Checking for Asynchronous Boolean Programs. 75-90
Dragan Bosnacki, Gerard J. Holzmann:
Improving Spin's Partial-Order Reduction for Breadth-First Search. 91-105
Vladimir Levin, Robert Palmer, Shaz Qadeer, Sriram K. Rajamani:
Sound Transaction-Based Reduction Without Cycle Detection. 106-122

Dealing with Complex Data

Sarfraz Khurshid, Iván García, Yuk Lai Suen:
Repairing Structurally Complex Data. 123-138
Yung-Pin Cheng:
Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices. 139-153
Tomás Barros, Ludovic Henrio, Eric Madelaine:
Behavioural Models for Hierarchical Components. 154-168

Checking Temporal Properties

Jean-Michel Couvreur, Alexandre Duret-Lutz, Denis Poitrenaud:
On-the-Fly Emptiness Checks for Generalized Büchi Automata. 169-184
Bas Luttik, Nikola Trcka:
Stuttering Congruence for chi. 185-199
Salamah Salamah, Ann Q. Gates, Steve Roach, Oscar Mondragon:
Verifying Pattern-Generated LTL Formulas: A Case Study. 200-220

Checking Security and Real-Time Properties

Abdul Sahid Khan, Madhavan Mukund, S. P. Suresh:
Generic Verification of Security Protocols. 221-235
Gerrit Rothmaier, Tobias Kneiphoff, Heiko Krumm:
Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models. 236-250
Eric Mercer, Michael Jones:
Model Checking Machine Code with the GNU Debugger. 251-265

Tool Papers

Alastair F. Donaldson, Simon J. Gay:
Etch: An Enhanced Type Checking Tool for Promela. 266-271
Peter C. Dillinger, Panagiotis Manolios:
Enhanced Probabilistic Verification with 3Spin and 3Murphi. 272-276
Anil Madhavapeddy, David Scott, Richard Sharp:
SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions. 277-281
Dimitra Giannakopoulou, Corina S. Pasareanu:
Learning-Based Assume-Guarantee Verification (Tool Paper). 282-287