Frontmatter

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)


@InProceedings{SPIN14p1, author = {Hao Zheng}, title = {Local State Space Construction for Compositional Verification of Concurrent Systems}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p11, author = {Michael Emmi and Burcu Kulahcioglu Ozkan and Serdar Tasiran}, title = {Exploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {11-10}, doi = {}, year = {2014}, }

Toward Parameterized Verification of Synchronous Distributed Applications
Sagar Chaki and James Edmondson
(Carnegie Mellon University, USA)


@InProceedings{SPIN14p21, author = {Sagar Chaki and James Edmondson}, title = {Toward Parameterized Verification of Synchronous Distributed Applications}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {21-20}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p25, author = {Henning Günther and Georg Weissenbacher}, title = {Incremental Bounded Software Model Checking}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {25-24}, doi = {}, year = {2014}, }

Certification for Configurable Program Analysis
Marie-Christine Jakobs and Heike Wehrheim
(University of Paderborn, Germany)


@InProceedings{SPIN14p35, author = {Marie-Christine Jakobs and Heike Wehrheim}, title = {Certification for Configurable Program Analysis}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {35-34}, doi = {}, year = {2014}, }

SpinCause: A Tool for Causality Checking
Florian Leitner-Fischer and Stefan Leue
(University of Konstanz, Germany)


@InProceedings{SPIN14p45, author = {Florian Leitner-Fischer and Stefan Leue}, title = {SpinCause: A Tool for Causality Checking}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {45-44}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p49, author = {Zmago Brezočnik and Boštjan Vlaovič and Aleksander Vreže}, title = {SpinRCP: The Eclipse Rich Client Platform Integrated Development Environment for the Spin Model Checker}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {49-48}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p53, author = {Ezio Bartocci and Richard DeFrancisco and Scott A. Smolka}, title = {Towards a GPGPU-Parallel SPIN Model Checker}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {53-52}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p63, author = {Ioannis Filippidis and Gerard J. Holzmann}, title = {An Improvement of the Piggyback Algorithm for Parallel Model Checking}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {63-62}, doi = {}, year = {2014}, }

TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata
Robin P. Neatherway and C.-H. Luke Ong
(University of Oxford, UK)


@InProceedings{SPIN14p73, author = {Robin P. Neatherway and C.-H. Luke Ong}, title = {TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {73-72}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p77, author = {Pavel Parízek and Pavel Jančík}, title = {Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {77-76}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p87, author = {František Blahoudek and Alexandre Duret-Lutz and Mojmír Křetínský and Jan Strejček}, title = {Is There a Best Büchi Automaton for Explicit Model Checking?}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {87-86}, doi = {}, year = {2014}, }

Automatic Handling of Native Methods in Java PathFinder
Nastaran Shafiei and Franck van Breugel
(NASA Ames Research Center, USA; York University, Canada)


@InProceedings{SPIN14p97, author = {Nastaran Shafiei and Franck van Breugel}, title = {Automatic Handling of Native Methods in Java PathFinder}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {97-96}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p101, author = {Noomene Ben Henda}, title = {Generic and Efficient Attacker Models in SPIN}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {101-100}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p111, author = {Quoc-Sang Phan and Pasquale Malacaria and Corina S. Păsăreanu and Marcelo d'Amorim}, title = {Quantifying Information Leaks using Reliability Analysis}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {111-110}, doi = {}, year = {2014}, }

Unit Testing for SPIN: runspin and parsepan
Theo C. Ruys
(RUwise, Netherlands)


@InProceedings{SPIN14p115, author = {Theo C. Ruys}, title = {Unit Testing for SPIN: runspin and parsepan}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {115-114}, doi = {}, year = {2014}, }

Verige: Verification with Invariant Generation Engine
Nicolas Latorre, Francesco Alberti, and Natasha Sharygina
(University of Lugano, Switzerland)


@InProceedings{SPIN14p119, author = {Nicolas Latorre and Francesco Alberti and Natasha Sharygina}, title = {Verige: Verification with Invariant Generation Engine}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {119-118}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p123, author = {Aditya Thakur and Jason Breck and Thomas Reps}, title = {Satisfiability Modulo Abstraction for Separation Logic with Linked Lists}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {123-122}, doi = {}, year = {2014}, }

CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko
(TU München, Germany; Microsoft Research, UK)


@InProceedings{SPIN14p133, author = {Tewodros A. Beyene and Marc Brockschmidt and Andrey Rybalchenko}, title = {CTL+FO Verification as Constraint Solving}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {133-132}, doi = {}, year = {2014}, }

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)


@InProceedings{SPIN14p137, author = {Allison Sullivan and Razieh Nokhbeh Zaeem and Sarfraz Khurshid and Darko Marinov}, title = {Towards a Test Automation Framework for Alloy}, booktitle = {Proc.\ SPIN}, publisher = {ACM}, pages = {137-136}, doi = {}, year = {2014}, }

proc time: 0.66