Write a Blog >>
SPIN 2017
co-located with ISSTA 2017

Full Papers

  • Matthieu Renard, Antoine Rollet and Ylies Falcone. Runtime Enforcement Using Büchi Games
  • Daniel Ratiu and Andreas Ulrich. Increasing Usability of Spin-based C Code Verification Using a Harness Definition Language
  • Srinivas Pinisetty, Partha Roop, Steven Smyth, Stavros Tripakis and Reinhard von Hanxleden. Runtime enforcement of reactive systems using synchronous enforcers
  • Wytse Oortwijn, Tom van Dijk and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability
  • Heila Botha, Oksana Tkachuk, Brink Van Der Merwe and Willem Visser. Addressing Challenges In Obtaining High Coverage When Model Checking Android Applications
  • Guangyuan Li, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen. Practical Controller Synthesis for MTL_{0,\infty}
  • John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan and Dominik Wojtczak. An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space
  • Thomas Geffroy, Jérôme Leroux and Grégoire Sutre. Backward Coverability with Pruning for Lossy Channel Systems
  • Paul Fiterau-Brostean, Frits Vaandrager, Erik Poll, Joeri de Ruiter, Toon Lenaerts and Patrick Verleg. Model Learning and Model Checking of SSH Implementations
  • Michalis Kokologiannakis and Konstantinos Sagonas. Stateless Model Checking of the Linux Kernel’s Hierarchical Read-Copy-Update (Tree RCU)
  • Idress Husien, Nicolas Berthier and Sven Schewe. A Hot Method for Synthesising Cool Controllers
  • Huu Vu Nguyen and Tayssir Touili. CARET Model Checking for Malware Detection
  • Jinru Hua and Sarfraz Khurshid. Sketch4J: Execution-Driven Sketching for Java
  • Nima Dini, Cagdas Yelen and Sarfraz Khurshid. Optimizing Parallel Korat Using Invalid Ranges
  • Pouria Mellati, Ehsan Khamespanah and Ramtin Khosravi. LeeTL: LTL with Quantifications Over Model Objects
  • Vincent Bloemen, Alexandre Duret-Lutz and Jaco van de Pol. Explicit State Model Checking with Generalized Büchi and Rabin Automata

Short Papers

  • Lucas Wagner, David Greve and Andrew Gacek. SIMPAL: A Compositional Reasoning Framework for Imperative Programs
  • Marco Antonio Feliu Gabaldon, Camilo Rocha and Swee Balachandran. Verification-driven Development of Icarous Based on Automatic Reachability Analysis
  • Blake Loring, Duncan Mitchell and Johannes Kinder. ExpoSE: Practical Symbolic Execution of Standalone JavaScript
  • Laura Panizo, Alberto Salmerón, Maria Del Mar Gallardo and Pedro Merino. Guided Test Case Generation for Mobile Apps in the TRIANGLE Project
  • Marcello M. Bersani, Madalina Erascu, Francesco Marconi, Silvio Ghilardi and Matteo Rossi. Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories