Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state of the art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods – neural network compression and an autoencoder-based deep learning architecture for training Koopman operators for the purpose of trajectory prediction. ... Read more

Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments. ... Read more

Cyber-physical systems integrate digital control and physical processes and often operate in complex, uncertain environments. The consequence of operational failures in such systems can be catastrophic and may include loss of life, environmental damage, irreparable system damage, and economic disruption. Therefore, safety is a critical concern and traditional engineering approaches that only rely on extensive testing and conservative design margins are insufficient to guarantee safety in the face of uncertainty. The issue is that testing only assesses the performance on a limited number of scenarios or samples, while in practice the collection of possible scenarios is uncountable due to the physical process and uncertainties therein. Formal methods provide a powerful alternative, offering mathematically rigorous verification that accounts for all possible behaviours subject to ranges of disturbances and uncertainties. A key challenge in applying formal methods to stochastic dynamical systems is a fundamental tension between computational tractability and conservatism. Existing approaches either scale poorly with the system dimension and complexity or produce loose bounds on safety probabilities that limit their practical applicability. This creates a critical gap between theory and practice: while formal verification methods exist, their practical applicability to real-world systems remains severely limited. Therefore, the core research question driving this work is: How to efficiently compute tight bounds on the satisfaction probabilities for safety, reachability, and reach-avoid specifications of stochastic systems?

To answer this question and address the gap, the present dissertation develops several complementary approaches for efficiently verifying properties of stochastic systems. The focus is on discrete-time, continuous-space stochastic systems and simple specifications over given sets. The approaches represent points along the spectrum of the scalability-conservatism trade-off and rely on different system assumptions. The methods developed belong to two families: stochastic barrier functions and finite-state abstractions.

Stochastic barrier functions are Lyapunov-like functions that provide certificates of safety by imposing conditions on the expected value of the barrier function along system trajectories. The core idea is that if the composition of the barrier function with the dynamics of the system forms a c-martingale, then the probability of safety can be bounded using martingale inequalities. The main challenge is to construct a barrier that is optimal with respect to the martingale inequalities. Hand-crafting such functions is difficult and time-consuming, and existing synthesis methods are often limited to low-dimensional and simple systems for non-trivial results. To enable efficient synthesis of stochastic barrier functions, we develop multiple synthesis techniques, including a neural network-based method that offers flexibility but requires post hoc verification to confirm correctness. More significantly, we introduce piecewise-constant stochastic barrier function theory and synthesis methods that are guaranteed to asymptotically approach optimality. The synthesis methods include a dual linear programming formulation, a counterexample-guided inductive synthesis with linear programming solvers, and gradient descent optimization; their trade-off is between scalability and required parameter tuning. The theoretical analysis of piece-wise constant barriers reveals deep insights into the relationship between barrier functions and system dynamics, illuminates fundamental sources of conservatism inherent to the approach, and establishes clear connections to Interval Markov Decision Process (IMDP)-based finite-state abstractions. Additionally, we develop a data-driven scenario-theoretic approach for systems with partially unknown dynamics, leveraging scenario theory to handle uncertainty in system models.

Finite-state abstractions, on the other hand, reduce the original continuous-space system to a finite-state model that can be analysed using probabilistic model checking techniques. While abstraction-based methods are exceedingly flexible -- they have been successfully applied to a wide range of systems, including partially-unknown systems, and specifications -- they often suffer from high computational complexity of using probabilistic model checking and scalability issues due to the pervasive state-space explosion problem.  To address the first issue, we develop hardware-aware algorithmic innovations for faster model checking of IMDPs via dynamic programming. Dynamic programming over IMDPs relies for efficiency on an algorithm named O-maximization, or order-maximization, which by theoretical analysis is revealed to be composed of two phases: a sorting phase and a cumulative summation phase. We introduce parallel algorithms to both phases, which allows us to exploit modern highly parallel computing architectures to achieve significant speedups in verifying IMDPs. To address the second issue, we introduce a novel finite-state model called factored Interval Markov Decision Processes (fIMDPs) that exploits structural properties of the system dynamics to significantly reduce memory requirements while maintaining formal guarantees. Factored models encode data-dependencies more fine-grained than flat models, which is the key driver for the reduction in memory. Moreover, factored models have been successfully used in the context of abstraction to Markov Decision Processes (MDPs), but have not been applied until now to IMDPs. An insight of abstracting to factored models is that the structural exploitation inadvertently tightens the ambiguity sets that characterize IMDPs conservatism, thereby reducing the pessimism of the bounds.

The methods developed in this dissertation represent significant algorithmic and theoretical advances to address the scalability-conservatism trade-off and enable more efficient computation of tighter safety probability bounds, advancing formal verification of stochastic dynamical systems. By advancing stochastic barrier function synthesis and IMDP-based finite-state abstractions, this work pushes the frontier of formal verification for stochastic systems, providing new tools and insights to bridge the gap between theory and practice.  The findings suggest that future progress in scalable safety verification for stochastic systems depends critically on designing algorithms that respect and exploit inherent problem structure, offering a promising, albeit challenging path toward making formal methods practical for real-world stochastic cyber-physical systems. ... Read more

Stochastic barrier functions (SBFs) are Lyapunov-like functions that enable safety analysis of stochastic systems. Finding a valid SBF, however, is challenging, as it requires solving a complex functional optimization problem. Existing convex approaches are often limited to low-dimensional systems with simple (polynomial) dynamics, while non-convex approaches lack completeness guarantees. To address these challenges, this paper presents a novel SBF synthesis framework based on piecewise (PW) functions We first outline a general formulation of PW-SBFs. Then, we focus on PW-Constant (PWC) SBFs and show how their simplicity yields computational advantages for general stochastic systems. Specifically, we prove that synthesis of PWC-SBFs reduces to a minimax optimization problem. We then introduce three efficient algorithms to solve this problem, each offering distinct trade-offs, all with completeness guarantees. The first algorithm is based on dual linear programming (LP), which provides an exact solution to the minimax optimization problem. The second is a more scalable algorithm based on counter-example guided inductive synthesis, which involves solving two smaller LPs. The third algorithm solves the minimax problem using gradient descent, which admits even better scalability. We provide an extensive evaluation of these methods on various case studies, including neural network dynamic models, nonlinear switched systems, and high-dimensional linear systems. Our benchmarks demonstrate that PWC-SBFs outperform state-of-the-art methods, namely sum-of-squares and neural barrier functions, and can scale to eight dimensional systems. ... Read more

This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results. ... Read more

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025. ... Read more

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025. ... Read more

This paper introduces a method of identifying a maximal set of safe strategies from data for stochastic systems with unknown dynamics using barrier certificates. The first step is learning the dynamics of the system via Gaussian Process (GP) regression and obtaining probabilistic errors for this estimate. Then, we develop an algorithm for constructing piecewise stochastic barrier functions to find a maximal permissible strategy set using the learned GP model, which is based on sequentially pruning the worst controls until a maximal set is identified. The permissible strategies are guaranteed to maintain probabilistic safety for the true system. This is especially important for learned systems, because a rich strategy space enables additional data collection and complex behaviors while remaining safe. Case studies on linear and nonlinear systems demonstrate that increasing the size of the dataset for learning grows the permissible strategy set. ... Read more

Autonomous vehicles rely on accurate trajectory prediction to inform decision-making processes related to navigation and collision avoidance. However, current trajectory prediction models show signs of overfitting, which may lead to unsafe or suboptimal behavior. To address these challenges, this paper presents a comprehensive framework that categorizes and assesses the definitions and strategies used in the literature on evaluating and improving the robustness of trajectory prediction models. This involves a detailed exploration of various approaches, including data slicing methods, perturbation techniques, model architecture changes, and post-training adjustments. In the literature, we see many promising methods for increasing robustness, which are necessary for safe and reliable autonomous driving. ... Read more

In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis of probabilistic models, such as PRISM. A key feature of IntervalMDP.jl is that it presents both a multi-threaded CPU and a GPU-accelerated implementation of value iteration algorithms for IMDPs. In particular, IntervalMDP.jl takes advantage of the Julia type system and the inherently parallelizable nature of value iteration to improve the efficiency of performing analysis of IMDPs. On a set of examples, we show that IntervalMDP.jl substantially outperforms existing tools for verification and strategy synthesis for IMDPs in both computation time and memory consumption. ... Read more

Control Barrier Functions (CBFs) that provide formal safety guarantees have been widely used for safety-critical systems. However, it is non-trivial to design a CBF. Utilizing neural networks as CBFs has shown great success, but it necessitates their certification as CBFs. In this work, we leverage bound propagation techniques and the Branch-and - Bound scheme to efficiently verify that a neural network satisfies the conditions to be a CBF over the continuous state space. To accelerate training, we further present a framework that embeds the verification scheme into the training loop to synthesize and verify a neural CBF simultaneously. In partic-ular, we employ the verification scheme to identify partitions of the state space that are not guaranteed to satisfy the CBF conditions and expand the training dataset by incorporating additional data from these partitions. The neural network is then optimized using the augmented dataset to meet the CBF conditions. We show that for a non-linear control-affine system, our framework can efficiently certify a neural network as a CBF and render a larger safe set than state-of-the-art neural CBF works. We further employ our learned neural CBF to derive a safe controller to illustrate the practical use of our framework. ... Read more

Providing non-trivial certificates of safety for non-linear stochastic systems is an important open problem. One promising solution to address this problem is the use of barrier functions. Barrier functions are functions whose composition with the system forms a Martingale and enable the computation of the probability that the system stays within a safe set over a finite time horizon. However, existing approaches to find barrier functions generally restrict the search to a small class of functions, often leading to conservatism. To address this problem, in this letter, we parameterize barrier functions as neural networks and show that bound propagation techniques and linear programming can be successfully employed to find Neural Barrier Functions. Further, we develop a branch-and-bound scheme based on linear relaxations that improves the scalability of the proposed framework. On several case studies we show that our approach scales to neural networks of hundreds of neurons and multiple hidden layers and often produces certificates of safety that are tighter than state-of-the-art methods. ... Read more

This paper proposes a new framework to compute finite-horizon safety guarantees for discrete-time piece-wise affine systems with stochastic noise of unknown distributions. The approach is based on a novel approach to synthesise a stochastic barrier function (SBF) from noisy data and rely on the scenario optimization theory. In particular, we show that the stochastic program to synthesize a SBF can be relaxed into a chance-constrained optimisation problem on which scenario approach theory applies. We further show that the resulting program can be reduced to a linear programming problem, thus guaranteeing efficiency. In contrast to existing approaches, this method is data efficient as it only requires the number of data to be proportional to the logarithm in the negative inverse of the confidence level and is computationally efficient due to its reduction to linear programming. The efficacy of the method is empirically evaluated on various verification benchmarks. Experiments show a significant improvement with respect to state-of-the-art, obtaining tighter certificates with a confidence that is several orders of magnitude higher. ... Read more

Hamiltonian systems represent an important class of dynamical systems such as pendulums, molecular dynamics, and cosmic systems. The choice of solvers is significant to the accuracy when simulating Hamiltonian systems, where symplectic solvers show great significance. Recent advances in neural network-based hypersolvers, though achieve competitive results, still lack the symplecity necessary for reliable simulations, especially over long time horizons. To alleviate this, we introduce Hyperverlet, a new hypersolver composing the traditional, symplectic velocity Verlet and symplectic neural network-based solvers. More specifically, we propose a parameterization of symplectic neural networks and prove that hyperbolic tangent is r-finite expanding the set of allowable activation functions for symplectic neural networks, improving the accuracy. Extensive experiments on a spring-mass and a pendulum system justify the design choices and suggest that Hyperverlet outperforms both traditional solvers and hypersolvers. ... Read more