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