2015 International SPIN Symposium on Model Checking of Software

held August 24-26, 2014, in Stellenbosch, South-Africa.
Invited Talks
String Analysis for Vulnerability Detection and Repair , Tevfik Bultan (UC Santa Barbara, USA)
The Augmented Reality of Model Counting , Willem Visser (Stellenbosch University, S. Africa)

Tutorial
CBMC: Bounded Model Checking of Concurrent Programs , Michael Tautschnig (Oxford University, UK)

Research Papers
[PDF] Parallel SAT-Based Parameterised Three-Value Model Checking, N. Timm, S. Fruner, P. Sibanda
[PDF] Symbolic Causality Checking Using Bounded Model Checking, A. Beer, S. Heidinger, U. Kuhne, F. Leitner-Fisher, S. Leueu
[PDF] On Refinement of Buchi Automata for Explicit Model Checking, F. Blahoudek, A. Duret-Lutz, V. Rujbr, J. Strejcek
[PDF] Comparitive Analysis of Leakage Tools on Scalable Case Studies, F. Biondi, A. Legay, J. Quilbeuf
[PDF] MESS: Memory Performance Debuggin on Embedded Multi-Core Systems, S. Chattopaghyah
[PDF] Fast, Dynamically-Sized Concurrent Hash-Table, J. Barnat, P. Rockai, V. Still, J. Weiser
[PDF] Practical Stutter-Invariant Checks for omega-Regular Languages, T. Michaud, A. Duret-Lutz
[PDF] Model Counting for Complex Data Structures, A. Filieri, M.F. Frias, C.S. Pasareanu, W. Visser
[PDF] Family-Based Model Checking without a Family-Based Model Checker, A.S. Dimovski, A.S. Al-Sibahi, C. Brabrand, A. Wasowski
[PDF] Runtime Verification of Expected Energy Consumption in Smartphones, A.R. Espada, M. del Mar Gallardo, A. Samleron, P. Merino
[PDF] Refinement Selection, D. Beyer, S. Lowe, P. Wendler
[PDF] Benchmarking and Resource Measurement - Application to Automatic Verification, D. Beyer, S. Lowe, P. Wendler
[PDF] Picklock: a Deadlock Prediction Approach under Nested Locking, F. Sorrentino
[PDF] IC-Cut: a Compositional Search Strategy for Dynamic Test Generation, M. Christakis, P. Godefroid

Tool & Idea Papers
[PDF] ASTRA: A tool for Abstract Interpretation of Graph Transformation Systems, P. Backes, J. Reineke
[PDF] Directed Model Checking for Promela with Relaxation-Based Distance Functions, A.S. Andisha, M. Wehrle, B. Westphal
[PDF] DSVerifier: A Bounded Model Checking Tool for Digital Systems, H. Ismail, I. Bessa, L. Cordeiro, E. Batista de Lima Filho, J.E. Chaves Filho
[PDF] From Helena Ensemble Specifications to Promela Verification Models, A. Klarl

Spin Homepage
Spin Symposia