SPIN 2017 – Proceedings

24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (SPIN 2017), July 13–14, 2017, Santa Barbara, CA, USA

Frontmatter

Message from the Chairs
Article: spin17foreword-fm001-p (type: Frontmatter) doi:

SPIN 2017 Organization
Article: spin17foreword-fm002-p (type: Frontmatter) doi:

Invited Papers

Cobra: Fast Structural Code Checking (Keynote)
Gerard J. Holzmann
(Nimble Research, USA)
Article: spin17key-key1-p (type: Invited Talk Paper) doi:

Automated Formal Reasoning about Amazon Web Services (Keynote)
Byron Cook
(Amazon Web Services, USA; University College London, UK)
Article: spin17key-key3-p (type: Invited Talk Paper) doi:

SunDew: Systematic Automated Security Testing (Keynote)
Domagoj Babic
(Google, USA)
Article: spin17key-key2-p (type: Invited Talk Paper) doi:

Reports

The RERS 2017 Challenge and Workshop (Invited Paper)
Marc Jasper, Maximilian Fecke, Bernhard Steffen, Markus Schordan, Jeroen Meijer, Jaco van de Pol, Falk Howar, and Stephen F. Siegel
(Lawrence Livermore National Laboratory, USA; TU Dortmund, Germany; University of Twente, Netherlands; TU Clausthal, Germany; University of Delaware, USA)
Article: spin17inv-inv1-p (type: Invited Talk Paper) doi:

Symbolic Verification

Distributed Binary Decision Diagrams for Symbolic Reachability
Wytse Oortwijn, Tom van Dijk, and Jaco van de Pol
(University of Twente, Netherlands; JKU Linz, Austria)
Article: spin17main-mainid17-p (type: Full Paper) doi:

Model Checking I

Addressing Challenges in Obtaining High Coverage When Model Checking Android Applications
Heila Botha, Oksana Tkachuk, Brink van der Merwe, and Willem Visser
(Stellenbosch University, South Africa; NASA Ames Research Center, USA)
Article: spin17main-mainid20-p (type: Full Paper) doi:

LeeTL: LTL with Quantifications over Model Objects
Pouria Mellati, Ehsan Khamespanah, and Ramtin Khosravi
(University of Tehran, Iran; Reykjavik University, Iceland)
Article: spin17main-mainid47-p (type: Full Paper) doi:

Explicit State Model Checking with Generalized Büchi and Rabin Automata
Vincent Bloemen, Alexandre Duret-Lutz, and Jaco van de Pol
(University of Twente, Netherlands; LRDE, France)
Article: spin17main-mainid48-p (type: Full Paper) doi:

Code Verification

Runtime Enforcement

Runtime Enforcement using Büchi Games
Matthieu Renard, Antoine Rollet, and Yliès Falcone
(LaBRI, France; Bordeaux INP, France; University of Bordeaux, France; Grenoble Alpes University, France; Inria, France; CNRS, France; Laboratoire d'Informatique de Grenoble, France)
Article: spin17main-mainid7-p (type: Full Paper) doi:

Runtime Enforcement of Reactive Systems using Synchronous Enforcers
Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Stavros Tripakis, and Reinhard von Hanxleden
(Aalto University, Finland; University of Gothenburg, Sweden; University of Auckland, New Zealand; University of Kiel, Germany; University of California at Berkeley, USA)
Article: spin17main-mainid12-p (type: Full Paper) doi:

Model Checking - Short Papers

SIMPAL: A Compositional Reasoning Framework for Imperative Programs
Lucas Wagner, David Greve, and Andrew Gacek
(Iowa State University, USA; Rockwell Collins, USA)
Article: spin17main-mainid11-p (type: Short Paper) doi:

Verification-Driven Development of ICAROUS Based on Automatic Reachability Analysis: A Preliminary Case Study
Marco A. Feliú, Camilo Rocha, and Swee Balachandran
(National Institute of Aerospace, USA; Pontificia Universidad Javeriana, Colombia)
Article: spin17main-mainid14-p (type: Short Paper) doi:

Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories
Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu, and Silvio Ghilardi
(Politecnico di Milano, Italy; Institute e-Austria Timisoara, Romania; West University of Timisoara, Romania; University of Milan, Italy)
Article: spin17main-mainid43-p (type: Short Paper) doi:

Program Synthesis

Practical Controller Synthesis for MTL_0,∞
Guangyuan Li, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, and Danny Bøgsted Poulsen
(Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Aalborg University, Denmark; Inria, France; University of Kiel, Germany)
Article: spin17main-mainid23-p (type: Full Paper) doi:

An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space
John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, and Dominik Wojtczak
(University of Liverpool, UK; National University of Singapore, Singapore)
Article: spin17main-mainid27-p (type: Full Paper) doi:

A Hot Method for Synthesising Cool Controllers
Idress Husien, Nicolas Berthier, and Sven Schewe
(University of Liverpool, UK)
Article: spin17main-mainid35-p (type: Full Paper) doi:

Model Checking II

Backward Coverability with Pruning for Lossy Channel Systems
Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre
(University of Bordeaux, France; CNRS, France; LaBRI, France)
Article: spin17main-mainid29-p (type: Full Paper) doi:

Model Learning and Model Checking of SSH Implementations
Paul Fiterău-Broştean, Toon Lenaerts, Erik Poll, Joeri de Ruiter, Frits Vaandrager, and Patrick Verleg
(Radboud University Nijmegen, Netherlands)
Article: spin17main-mainid30-p (type: Full Paper) doi:

CARET Model Checking for Malware Detection
Huu-Vu Nguyen and Tayssir Touili
(University of Paris Diderot, France; LIPN, France; CNRS, France; University of Paris North, France)
Article: spin17main-mainid37-p (type: Full Paper) doi:

Program Sketching

EdSketch: Execution-Driven Sketching for Java
Jinru Hua and Sarfraz Khurshid
(University of Texas at Austin, USA)
Article: spin17main-mainid41-p (type: Full Paper) doi:

Testing

Stateless Model Checking of the Linux Kernel's Hierarchical Read-Copy-Update (Tree RCU)
Michalis Kokologiannakis and Konstantinos Sagonas
(National Technical University of Athens, Greece; Uppsala University, Sweden)
Article: spin17main-mainid31-p (type: Full Paper) doi:

Optimizing Parallel Korat Using Invalid Ranges
Nima Dini, Cagdas Yelen, and Sarfraz Khurshid
(University of Texas at Austin, USA)
Article: spin17main-mainid45-p (type: Full Paper) doi:

Testing - Short Papers

Guided Test Case Generation for Mobile Apps in the TRIANGLE Project: Work in Progress
Laura Panizo, Alberto Salmerón, María-del-Mar Gallardo, and Pedro Merino
(University of Málaga, Spain)
Article: spin17main-mainid22-p (type: Short Paper) doi:

ExpoSE: Practical Symbolic Execution of Standalone JavaScript
Blake Loring, Duncan Mitchell, and Johannes Kinder
(Royal Holloway University of London, UK)
Article: spin17main-mainid34-p (type: Short Paper) doi: