SPIN 2014 – Proceedings

2014 International SPIN Symposium on Model Checking of Software (SPIN), July 21–23, 2014, San Jose, CA, USA

Frontmatter

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

Organization
Article: spin14foreword-fm002-p (type: Frontmatter) doi:

Concurrent, Synchronous, and Asynchronous Systems
Mon, Jul 21, 10:30 - 11:50, Santa Clara Room (Chair: Willem Visser)

Local State Space Construction for Compositional Verification of Concurrent Systems
Hao Zheng
(University of South Florida, USA)
Article: spin14main-mainid3-p (type: Full Paper (10 pages)) doi:

Exploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs
Michael Emmi, Burcu Kulahcioglu Ozkan, and Serdar Tasiran
(IMDEA Software Institute, Spain; Koç University, Turkey)
Article: spin14main-mainid32-p (type: Full Paper (10 pages)) doi:

Toward Parameterized Verification of Synchronous Distributed Applications
Sagar Chaki and James Edmondson
(Carnegie Mellon University, USA)
Article: spin14main-mainid22-p (type: Short Paper (4 pages)) doi:

Model Checking I
Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Incremental Bounded Software Model Checking
Henning Günther and Georg Weissenbacher
(Vienna University of Technology, Austria)
Article: spin14main-mainid26-p (type: Full Paper (10 pages)) doi:

Certification for Configurable Program Analysis
Marie-Christine Jakobs and Heike Wehrheim
(University of Paderborn, Germany)
Article: spin14main-mainid4-p (type: Full Paper (10 pages)) doi:

SpinCause: A Tool for Causality Checking
Florian Leitner-Fischer and Stefan Leue
(University of Konstanz, Germany)
Article: spin14main-mainid2-p (type: Short Paper (4 pages)) doi:

SpinRCP: The Eclipse Rich Client Platform Integrated Development Environment for the Spin Model Checker
Zmago Brezočnik, Boštjan Vlaovič, and Aleksander Vreže
(University of Maribor, Slovenia)
Article: spin14main-mainid14-p (type: Short Paper (4 pages)) doi:

Parallel and Higher-Order Verification
Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Towards a GPGPU-Parallel SPIN Model Checker
Ezio Bartocci, Richard DeFrancisco, and Scott A. Smolka
(Vienna University of Technology, Austria; Stony Brook University, USA)
Article: spin14main-mainid24-p (type: Full Paper (10 pages)) doi:

An Improvement of the Piggyback Algorithm for Parallel Model Checking
Ioannis Filippidis and Gerard J. Holzmann
(California Institute of Technology, USA; Jet Propulsion Laboratory, USA)
Article: spin14main-mainid27-p (type: Full Paper (10 pages)) doi:

TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata
Robin P. Neatherway and C.-H. Luke Ong
(University of Oxford, UK)
Article: spin14main-mainid13-p (type: Short Paper (4 pages)) doi:

Model Checking II
Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)

Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal
Pavel Parízek and Pavel Jančík
(Charles University, Czech Republic)
Article: spin14main-mainid7-p (type: Full Paper (10 pages)) doi:

Is There a Best Büchi Automaton for Explicit Model Checking?
František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejček
(Masaryk University, Czech Republic; LRDE EPITA, France)
Article: spin14main-mainid35-p (type: Full Paper (10 pages)) doi:

Automatic Handling of Native Methods in Java PathFinder
Nastaran Shafiei and Franck van Breugel
(NASA Ames Research Center, USA; York University, Canada)
Article: spin14main-mainid21-p (type: Short Paper (4 pages)) doi:

Testing and Security
Tue, Jul 22, 13:30 - 15:00, Santa Clara Room (Chair: Nastaran Shafiei)

Generic and Efficient Attacker Models in SPIN
Noomene Ben Henda
(Ericsson Research, Sweden)
Article: spin14main-mainid18-p (type: Full Paper (10 pages)) doi:

Quantifying Information Leaks using Reliability Analysis
Quoc-Sang Phan, Pasquale Malacaria, Corina S. Păsăreanu, and Marcelo d'Amorim
(Queen Mary University of London, UK; Carnegie Mellon University, USA; NASA Ames Research Center, USA; Federal University of Pernambuco, Brazil)
Article: spin14main-mainid10-p (type: Short Paper (4 pages)) doi:

Unit Testing for SPIN: runspin and parsepan
Theo C. Ruys
(RUwise, Netherlands)
Article: spin14main-mainid20-p (type: Short Paper (4 pages)) doi:

Verige: Verification with Invariant Generation Engine
Nicolas Latorre, Francesco Alberti, and Natasha Sharygina
(University of Lugano, Switzerland)
Article: spin14main-mainid15-p (type: Short Paper (4 pages)) doi:

Constraint-Based Analysis
Tue, Jul 22, 15:30 - 16:40, Santa Clara Room (Chair: Franjo Ivancic)

Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
Aditya Thakur, Jason Breck, and Thomas Reps
(University of Wisconsin-Madison, USA; GrammaTech, USA)
Article: spin14main-mainid33-p (type: Full Paper (10 pages)) doi:

CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko
(TU München, Germany; Microsoft Research, UK)
Article: spin14main-mainid31-p (type: Short Paper (4 pages)) doi:

Towards a Test Automation Framework for Alloy
Allison Sullivan, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, and Darko Marinov
(University of Texas at Austin, USA; University of Illinois at Urbana-Champaign, USA)
Article: spin14main-mainid37-p (type: Short Paper (4 pages)) doi:

SPIN 2014 – Proceedings

Frontmatter

Concurrent, Synchronous, and Asynchronous Systems Mon, Jul 21, 10:30 - 11:50, Santa Clara Room (Chair: Willem Visser)

Model Checking I Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Parallel and Higher-Order Verification Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Model Checking II Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)