SPIN 2017- Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

Full Citation in the ACM Digital Library

SESSION: Invited Papers

Cobra: fast structural code checking (keynote)

• Gerard J. Holzmann

Automated formal reasoning about amazon web services (keynote)

• Byron Cook

SunDew: systematic automated security testing (keynote)

• Domagoj Babic

SESSION: 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
• Stephen F. Siegel

SESSION: Symbolic Verification

Distributed binary decision diagrams for symbolic reachability

• Wytse Oortwijn
• Tom van Dijk
• Jaco van de Pol

SESSION: Model Checking I

Addressing challenges in obtaining high coverage when model checking Android applications

• Heila Botha
• Oksana Tkachuk
• Brink van der Merwe
• Willem Visser

LeeTL: LTL with quantifications over model objects

• Pouria Mellati
• Ehsan Khamespanah
• Ramtin Khosravi

Explicit state model checking with generalized Büchi and Rabin automata

• Vincent Bloemen
• Alexandre Duret-Lutz
• Jaco van de Pol

SESSION: Code Verification

Increasing usability of spin-based C code verification using a harness definition language: leveraging model-driven code checking to practitioners

• Daniel Ratiu
• Andreas Ulrich

SESSION: Runtime Enforcement

Runtime enforcement using Büchi games

• Matthieu Renard
• Antoine Rollet
• Yliès Falcone

Runtime enforcement of reactive systems using synchronous enforcers

• Srinivas Pinisetty
• Partha S. Roop
• Steven Smyth
• Stavros Tripakis
• Reinhard von Hanxleden

SESSION: Model Checking - Short Papers

SIMPAL: a compositional reasoning framework for imperative programs

• Lucas Wagner
• David Greve
• Andrew Gacek

Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study

• Marco A. Feliú
• Camilo Rocha
• Swee Balachandran

Formal verification of data-intensive applications through model checking modulo theories

• Marcello M. Bersani
• Francesco Marconi
• Matteo Rossi
• Madalina Erascu
• Silvio Ghilardi

SESSION: Program Synthesis

Practical controller synthesis for MTL_0,∞

• Guangyuan Li
• Peter Gjøl Jensen
• Kim Guldstrand Larsen
• Axel Legay
• Danny Bøgsted Poulsen

An ordered approach to solving parity games in quasi polynomial time and quasi linear space

• John Fearnley
• Sanjay Jain
• Sven Schewe
• Frank Stephan
• Dominik Wojtczak

A hot method for synthesising cool controllers

• Idress Husien
• Nicolas Berthier
• Sven Schewe

SESSION: Model Checking II

Backward coverability with pruning for lossy channel systems

• Thomas Geffroy
• Jérôme Leroux
• Grégoire Sutre

Model learning and model checking of SSH implementations

• Paul Fiterău-Broştean
• Toon Lenaerts
• Erik Poll
• Joeri de Ruiter
• Frits Vaandrager
• Patrick Verleg

CARET model checking for malware detection

• Huu-Vu Nguyen
• Tayssir Touili

SESSION: Program Sketching

EdSketch: execution-driven sketching for Java

• Jinru Hua
• Sarfraz Khurshid

SESSION: Testing

Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU)

• Michalis Kokologiannakis
• Konstantinos Sagonas

Optimizing parallel Korat using invalid ranges

• Nima Dini
• Cagdas Yelen
• Sarfraz Khurshid

SESSION: 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
• Pedro Merino

ExpoSE: practical symbolic execution of standalone JavaScript

• Blake Loring
• Duncan Mitchell
• Johannes Kinder