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

Phone Layout
No Pictures
Monday, July 21, 2014
Message from the Chairs
08:30 – 08:30, Santa Clara Room, Chairs: Neha Rungta and Oksana Tkachuk
Message from the Chairs
Neha Rungta and Oksana Tkachuk
(NASA Ames Research Center)
LADEE Flight Software: Verification Techniques (Keynote)
08:45 – 08:45, Santa Clara Room, Chair: Oksana Tkachuk
LADEE Flight Software: Verification Techniques (Keynote)
09:10 – 09:10, University Room
Concurrent, Synchronous, and Asynchronous Systems (SPIN)
10:30 – 10:30, Santa Clara Room, Chair: Willem Visser
Local State Space Construction for Compositional Verification of Concurrent Systems
Hao Zheng
(University of South Florida, USA)
Publisher's Version
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)
Publisher's Version
Toward Parameterized Verification of Synchronous Distributed Applications
Sagar Chaki and James Edmondson
(Carnegie Mellon University, USA)
Publisher's Version
Model Checking I (SPIN)
13:30 – 13:30, Santa Clara Room, Chair: Sarfraz Khurshid
Incremental Bounded Software Model Checking
Henning Günther and Georg Weissenbacher
(Vienna University of Technology, Austria)
Publisher's Version
Certification for Configurable Program Analysis
Marie-Christine Jakobs and Heike Wehrheim
(University of Paderborn, Germany)
Publisher's Version
SpinCause: A Tool for Causality Checking
Florian Leitner-Fischer and Stefan Leue
(University of Konstanz, Germany)
Publisher's Version
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)
Publisher's Version Info
Discussion (JAMAICA)
15:30 – 15:30, University Room
Overall discussion (in the fishbowl format) on how the presented techniques and approaches influence the ROI of testing. The main goal is to get a better overview of the presented subjects, their relationships and relevance in industry.
Parallel and Higher-Order Verification (SPIN)
15:40 – 15:40, 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)
Publisher's Version
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)
Publisher's Version
TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata
Robin P. Neatherway and C.-H. Luke Ong
(University of Oxford, UK)
Publisher's Version
Tuesday, July 22, 2014
Analysis of x86 Executables using Abstract Interpretation (Keynote)
08:45 – 08:45, Santa Clara Room, Chair: Neha Rungta
Analysis of x86 Executables using Abstract Interpretation (Keynote)
Model Checking II (SPIN)
10:30 – 10:30, 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)
Publisher's Version
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)
Publisher's Version
Automatic Handling of Native Methods in Java PathFinder
Nastaran Shafiei and Franck van Breugel
(NASA Ames Research Center, USA; York University, Canada)
Publisher's Version
Testing and Security (SPIN)
13:30 – 13:30, Santa Clara Room, Chair: Nastaran Shafiei
Generic and Efficient Attacker Models in SPIN
Noomene Ben Henda
(Ericsson Research, Sweden)
Publisher's Version
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)
Publisher's Version Preprint
Unit Testing for SPIN: runspin and parsepan
Theo C. Ruys
(RUwise, Netherlands)
Publisher's Version Preprint Info
Verige: Verification with Invariant Generation Engine
Nicolas Latorre, Francesco Alberti, and Natasha Sharygina
(University of Lugano, Switzerland)
Publisher's Version
Constraint-Based Analysis (SPIN)
15:30 – 15:30, 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)
Publisher's Version
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko
(TU München, Germany; Microsoft Research, UK)
Publisher's Version
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)
Publisher's Version
SPIN 2015 Announcement (SPIN)
16:40 – 16:40, Santa Clara Room
SPIN Banquet
18:00 – 18:00, Paolo’s Restaurant
333 W San Carlos St, #150, San Jose

Time stamp: 2020-10-20T22:59:22+02:00