Accepted Papers

Accepted Papers:

  • Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty Giovanni Bacci, Kim Guldstrand Larsen, Nicolas Markey, Patricia Bouyer-Decitre, Uli Fahrenberg and Pierre-Alain Reynier
  • A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm Laura Titolo, Mariano Moscato, Cesar Munoz, Aaron Dutle and Francois Bobot
  • A Weakness Measure for GR(1) Formulae Davide Giacomo Cavezza, Dalal Alrajeh and Andras Gyorgy
  • Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning Takumi Akazaki, Shuang Liu, Yoriyuki Yamagata, Yihai Duan and Jianye Hao
  • Modular Verification of Programs with Effects and Effect Handlers in Coq Thomas Letan, Yann Régis-Gianas, Pierre Chifflier and Guillaume Hiet
  • View abstraction for systems with component identities Gavin Low
  • Statistical Model Checking of LLVM Code Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen and Louis-Marie Traonouez
  • Stepwise Development and Model Checking of a Distributed Interlocking System – using RAISE Signe Geisler and Anne E. Haxthause
  • The Compound Interest in Relaxing Punctuality Thomas Ferrèr
  • Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenge, Evaluation and Recommendations Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham and Joost-Pieter Katoen
  • SDN-Actors: Modeling and Verification of SDN Programs Elvira Albert, Miguel Gomez-Zamalloa, Albert Rubio, Matteo Sammartino and Alexandra Silva
  • Deadlock Detection for Actor-based Coroutines Keyvan Azadbakht, Frank De Boer and Erik de Vink
  • CompoSAT: Specification-Guided Coverage for Model Finding Sorawee Porncharoenwase, Tim Nelson and Shriram Krishnamurthi
  • Encoding fairness in a synchronous concurrent program algebra Ian J. Hayes and Larissa Meinick
  • Combining Tools for Optimization and Analysis of Floating-Point Computations Pavel Panchekha, Zachary Tatlock, Eva Darulova and Heiko Becker
  • Approximate Partial Order Reduction Chuchu Fan, Zhenqi Huang and Sayan Mitra
  • Vector Barrier Certificates and Comparison Systems Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer
  • Towards ‘Verifying’ a Water Treatment System Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin and Zhiwu Xu
  • Dynamic Symbolic Verification of MPI Programs Dhriti Khanna, Subodh Sharma, César Rodríguez and Rahul Purandare
  • Timed Vacuity Hana Chockler, Shibashis Guha and Orna Kupferman
  • An Algebraic Approach for Reasoning About Information Flow Arthur Américo, Mario S. Alvim and Annabelle McIver
  • FSM Inference from Long Traces Florent Avellaneda and Alexandre Petrenk
  • QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems Andrea Vandin, Maurice H. Ter Beek, Axel Legay and Alberto Lluch Lafuente
  • To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation Sander de Putter and Anton Wijs
  • Compositional Reasoning for Shared-variable Concurrent Programs Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-Wei Lin and Jun Sun
  • Verifying Auto-Generated C Code from Simulink Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez and Thomas Rambow
  • IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl and David Garlan
  • Timed Epistemic Knowledge Bases for Social Networks Raúl Pardo, Cesar Sanchez and Gerardo Schneider
  • Multi-Robot LTL Planning Under Uncertainty Claudio Menghi, Sergio Garcia, Patrizio Pelliccione and Jana Tumova
  • Formal Specification and Verification of Dynamic Parametrized Architectures Alessandro Cimatti, Ivan Stojic and Stefano Tonetta
  • A lightweight deadlock analysis technique of object-oriented programs Cosimo Lanev
  • Producing Explanations for Rich Logics Simon Busard and Charles Pecheu
  • A wide-spectrum language for verification of programs on weak memory models Robert Colvin and Graeme Smit
  • Operational Semantics of a Weak Memory Model with Channel Synchronization Daniel Fava, Martin Steffen and Volker Stolz
  • Resource-aware Design for Reliable Autonomous Applications with Multiple Periods Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang and Kai Huang