Papers that have passed the repeatability evaluation present the RE-passed badge next to their title. Note that submitting the RE package was mandatory only for Tool and Case Study papers.

Regular papers

Daniel Liberzon and Hyungbo Shim.
Further Results on Stability of Linear Systems with Slow and Fast Time Variation and Switching

Eric Goubault and Sylvie Putot.
Inner and Outer Approximate Quantifier Elimination for General Reachability Problems

Swantje Plambeck, Aaron Bracht, Nemanja Hranisavljevic and Goerschwin Fey.
FaMoS– Fast Model Learning for Hybrid Cyber-Physical Systems using Decision Trees

Ashwani Anand, Satya Prakash Nayak and Anne-Kathrin Schmuck.
Contract-based Distributed Logical Controller Synthesis

Hui Jiang, Jianling Fu, Ming Xu, Yuxin Deng and Zhibin Li.
A Sample-Driven Solving Procedure for the Repeated Reachability of Quantum Continuous-time Markov Chains

Abolfazl Lavaei.
Abstraction-based Synthesis of Stochastic Hybrid Systems

Xiao Guo, Jianhua Zhao and Lei Bu.
Poles-based Invariant Generation for Verifying the BIBO Stability of Digital Filters

Rajab Aghamov, Christel Baier, Toghrul Karimov, Joel Ouaknine and Jakob Piribauer.
Linear Dynamical Systems with Continuous Weight Functions

Julien Calbert, Sébastien Mattenet, Antoine Girard and Raphaël Jungers.
Memoryless Concretization Relation

Yulong Gao, Karl H. Johansson and Alessandro Abate.
CTL Model Checking of MDPs over Distribution Spaces: Algorithms and Sampling-based Computations

Sebastian Schirmer, Jasdeep Singh, Emily Jensen, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan.
Temporal Behavior Trees: Robustness and Segmentation

Guillaume Berger, Masoumeh Ghanbarpour and Sriram Sankaranarayanan.
Cone-Based Abstract Interpretation for Nonlinear Positive Invariant Synthesis

Vishnu Murali, Ashutosh Trivedi and Majid Zamani.
Closure Certificates

Hussein Sibai and Enrique Mallada.
Recurrence of Nonlinear Control Systems: Entropy and Bit Rates

Yu Teng, Miaomiao Zhang and Jie An.
Learning Deterministic Multi-Clock Timed Automata

Guillaume Berger, Monal Narasimhamurthy and Sriram Sankaranarayanan.
Algorithms for Identifying Flagged and Guarded Linear Systems

Christian Abu-Mrad and Houssam Abbas.
Approximating the Geometry of Temporal Logic Formulas

Ameneh Nejati, Satya Prakash Nayak and Anne-Kathrin Schmuck.
Context-triggered Games for Reactive Synthesis over Stochastic Systems via Control Barrier Certificates

Carlos Andres Montenegro Gonzalez, Santiago Jimenez Leudo and Ricardo G. Sanfelice.
A Data-Driven Approach for Certifying Asymptotic Stability and Cost Evaluation for Hybrid Systems

Chaomin Jin, Xiaoxuan Ma, Tianxiang Ren, Wang Lin and Zuohua Ding.
Safe Controller Synthesis for Nonlinear Systems Using Bayesian Optimization Enhanced Reinforcement Learning

Bassem Ghorbel and Vinayak Prabhu.
Fast and Scalable Monitoring for Value-Freeze Operator augmented Signal Temporal Logic

Ruya Karagulle, Necmiye Ozay, Nikos Arechiga, Jonathan DeCastro and Andrew Best.
Incorporating Logic in Online Preference Learning for Safe Personalization of Autonomous Vehicles

Tool papers

Severin Bals, Alexandros Evangelidis, Jan Kretinsky and Jakob Waibel.
MULTIGAIN 2.0: MDP Controller Synthesis for Multiple Mean-payoff, LTL and Steady-state Constraints

Jun Liu, Yiming Meng, Maxwell Fitzsimmons and Ruikun Zhou.
LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction

Alec Edwards, Andrea Peruffo and Alessandro Abate.
Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

Stanley Bak, Sergiy Bogomolov, Abdelrahman Hekal, Niklas Kochdumper, Ethan Lew, Andrew Mata and Amir Rahmati.
Falsification using Reachability of Surrogate Koopman Models