Accepted Papers

  1. Optimal Proofs for Linear Temporal Logic on Lasso Words, David Basin, Bhargav Bhatt and Dmitriy Traytel.
  2. What’s to Come is Still Unsure: Synthesizing Controllers Resilient to Delayed Interaction, Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad and Naijun Zhan. 
  3. A Formally Verified Motion Planners for Autonomous Vehicles, Albert Rizaldi, Fabian Immler, Bastian Schürmann and Matthias Althoff.
  4. Robustness Testing of Intermediate Verifiers, Yu-Ting Chen and Carlo A. Furia.
  5. Simulation Algorithms for Symbolic Automata, Lukas Holik, Ondrej Lengal, Juraj Síč, Margus Veanes and Tomas Vojnar.
  6. Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems, Chih-Hong Cheng, Chung-Hao Huang and Hirotoshi Yasuoka.
  7. Recursive Online Enumeration of All Minimal Unsatisfiable Subsets, Jaroslav Bendík, Ivana Cerna and Nikola Benes.
  8. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode, Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio and Ilya Sergey.
  9. MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment, Bernd Finkbeiner, Christopher Hahn and Tobias Hans.
  10. Verifying Rust Programs with SMACK, Marek Baranowski, Shaobo He and Zvonimir Rakamaric.
  11. SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems, Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay and Saddek Bensalem.
  12. Synthesis in pMDPs: A Tale of 1001 Parameters, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu.
  13. Owl: A Library for Omega-Words, Automata, and LTL, Salomon Sickert, Jan Kretinsky and Tobias Meggendorfer.
  14. Temporal Logic Verification of Stochastic Systems Using Barrier Certificates, Pushpak Jagtap, Sadegh Soudjani and Majid Zamani.
  15. Bisimilarity Distances for Approximate Differential Privacy, Dmitry Chistikov, Andrzej Murawski and David Purser.
  16. A Symbolic Algorithm for Lazy Synthesis of Eager Strategies, Swen Jacobs and Mouhammad Sakr.
  17. Modular Verification of Concurrent Programs via Sequential Model Checking, Dan Rasin, Orna Grumberg and Sharon Shoham.
  18. Quantifiers on Demand, Arie Gurfinkel, Sharon Shoham and Yakir Vizel.
  19. Signal Convolution Logic, Simone Silvetti, Laura Nenzi, Ezio Bartocci and Luca Bortolussi.
  20. EVE: A Tool for Temporal Equilibrium Analysis, Julian Gutierrez, Muhammad Najib, Giuseppe Perelli and Michael Wooldridge.
  21. Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces, Bernard Boigelot and Isabelle Mainz.
  22. Accelerated Model Checking of Parametric Markov Chains, Paul Gainer, Ernst Moritz Hahn and Sven Schewe.
  23. Continuous-Time Markov Decisions based on Partial Exploration, Pranav Ashok, Yuliya Butkova, Holger Hermanns and Jan Kretinsky.
  24. A Fragment of Linear Temporal Logic for Universal Very Weak Automata, Keerthi Adabala and Rüdiger Ehlers.
  25. Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility, Anthony Lin and Rupak Majumdar.
  26. Round-Bounded Control of Parameterized Systems, Benedikt Bollig, Mathieu Lehaut and Nathalie Sznajder.
  27. PSense: Automatic Sensitivity Analysis for Probabilistic Programs, Zixin Huang, Zhenbang Wang and Sasa Misailovic.
  28. Information Leakage in Arbiter Protocols, Nestan Tsiskaridze, Lucas Bang, Joseph McMahan, Tevfik Bultan and Timothy Sherwood.
  29. Neural State Classification for Hybrid Systems, Dung Phan, Nicola Paoletti, Timothy Zhang, Radu Grosu, Scott Stoller and Scott Smolka.
  30. Bounded Synthesis of Reactive Programs, Carsten Gerstacker, Felix Klein and Bernd Finkbeiner.
  31. Maximum Realizability for Linear Temporal Logic Specifications, Rayna Dimitrova, Mahsa Ghasemi and Ufuk Topcu.
  32. Ranking and Repulsing Supermartingales for Approximating Reachability, Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe and Ichiro Hasuo.
  33. Reactive Synthesis of Register Transducers, Ayrat Khalimov, Benedikt Maderbacher and Roderick Bloem.