Program

Specification (Chair: Ina Schaeffer)

• From Software Specifications to Constraint Programming

  (Stefan Hallerstede, Miran Hasanagić, Sebastian Krings, Peter Gorm Larsen, and Michael Leuschel)

• Automated Specification Extraction and Analysis with Specstractor

  (Christoph Schulze, Rance Cleaveland, and Mikael Lindvall)

• Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation

  (Fahad Rafique Golra, Fabien Dagnat, Jeanine Souquières, Imen Sayar, and Sylvain Guerin)

Concurrency (Chair: Gwen Salün)

• Program Verification for Exception Handling on Active Objects Using Futures

  (Crystal Chang Din, Rudolf Schlatte, and Tzu-Chun Chen)

• Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems

  (Stefan Schupp and Erika Ábrahám)

• FASTLANE Is Opaque – a Case Study in Mechanized Proofs of Opacity

  (Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, and Heike Wehrheim)

Program Analysis (Chair: Heike Wehrheim)

• Monte Carlo Tree Search for Finding Costly Paths in Programs

  (Kasper Luckow, Corina S. Păsăreanu, and Willem Visser)

• A Cloud-Based Execution Framework for Program Analysis

  (Daniel Balasubramanian, Dmitriy Kostyuchenko, Kasper Luckow, Rody Kersten, and Gabor Karsai)

• Cross-Architecture Lifter Synthesis

  (Rijnard van Tonder and Claire Le Goues)

Model Checking and Runtime Verification (Chair: Crystal Chang Din)

• Counterexample Simplification for Liveness Property Violation

  (Gianluca Barbon, Vincent Leroy, and Gwen Salaün)

• Online Enumeration of All Minimal Inductive Validity Cores

  (Jaroslav Bendík, Elaheh Ghassabani, Michael Whalen, and Ivana Černá)

• Graph-Based Shape Analysis Beyond Context-Freeness

  (Hannah Arndt, Christina Jansen, Christoph Matheja, and Thomas Noll)

Applications (Chair: Rance Cleaveland)

• Formal Verification of Platoon Control Strategies

  (Adnan Rashid, Umair Siddique, and Osman Hasan)

• Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover

  (Catherine Dubois, Olga Grinchtein, Justin Pearson, and Mats Carlsson)

• Automated Validation of IoT Device Control Programs Through Domain-Specific Model Generation

  (Yunja Choi)

Shape Analysis and Reuse (Chair: Marc Pantel)

• Prevent: A Predictive Run-Time Verification Framework Using Statistical Learning

  (Reza Babaee, Arie Gurfinkel, and Sebastian Fischmeister)

• Facilitating Component Reusability in Embedded Systems with GPUs

  (Gabriel Campeanu)