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)

Automated formal reasoning about amazon web services (keynote)

SunDew: systematic automated security testing (keynote)

SESSION: Reports

The RERS 2017 challenge and workshop (invited paper)

SESSION: Symbolic Verification

Distributed binary decision diagrams for symbolic reachability

SESSION: Model Checking I

Addressing challenges in obtaining high coverage when model checking Android applications

LeeTL: LTL with quantifications over model objects

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

SESSION: Code Verification

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

SESSION: Runtime Enforcement

Runtime enforcement using Büchi games

Runtime enforcement of reactive systems using synchronous enforcers

SESSION: Model Checking - Short Papers

SIMPAL: a compositional reasoning framework for imperative programs

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

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

SESSION: Program Synthesis

Practical controller synthesis for MTL<sub>0,&#8734;</sub>

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

A hot method for synthesising cool controllers

SESSION: Model Checking II

Backward coverability with pruning for lossy channel systems

Model learning and model checking of SSH implementations

CARET model checking for malware detection

SESSION: Program Sketching

EdSketch: execution-driven sketching for Java

SESSION: Testing

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

Optimizing parallel Korat using invalid ranges

SESSION: Testing - Short Papers

Guided test case generation for mobile apps in the TRIANGLE project: work in progress

ExpoSE: practical symbolic execution of standalone JavaScript