2025-07-24 –, Main Room 1 (Main stage)
This talk demonstrates practical safety validation techniques from the new book "Algorithms for Validation" using Julia's ecosystem. Through interactive Pluto.jl notebooks and a case study of aircraft collision avoidance, we showcase Julia's capabilities in safety validation, including seamless integration with Python-based controllers and black-box simulation environments. No prior verification experience required!
As autonomous systems increasingly navigate our airways, roads, and critical infrastructure, the ability to rigorously validate their safety becomes crucial.
In this talk we will therefore be exploring safety validation, or "stress testing", of such dynamical systems, using a some of the algorithms presented in the new book "Algorithms for Validation" by M. Kochenderfer et. al. (available for free as pdf!)
As a case study, we will consider a system of two aircraft on a collision course, and a controller trying to avoid the collision.
A series of unfortunate observation errors may mislead the controller into making bad decisions, ultimately leading to a collision.
Finding such "rare failure events", and estimating their probability, is therefore integral for validating the integrity of the system and controller.
Through a series of interactive Pluto.jl notebooks we showcase how Julia can be used to (i) specify system safety properties, (ii) efficiently find rare failures by optimizing over system rollouts, (iii) estimating failure probabilities through Markov Chain Monte Carlo, and (iv) computing the reachable set through set propagation techniques (under bounded noise).
On the way, we make use of packages including SignalTemporalLogic.jl, NonlinearSolve.jl, Turing.jl, and LazySets.jl.
Even though the presented algorithms and used packages are implemented in Julia, we note that the environment and controller may be any black-box, and we showcase specifically how Julia may be used in conjunction with a Python based Neural Network controller, and a black-box simulation environment.
Although we highlight an example from aviation, similar problems arise in a wide range of applications such as autonomous driving and flight, financial decision making, chemical process control, logistics and transportation, energy grid balancing, and many others.
With this talk we therefore aim to inform practitioners about algorithmic developments for safety validation and the applicability through fast, flexible, and concise implementations in Julia.
No prior experience with verification is required, although a familiarity with dynamical systems or Markov decision processes may be beneficial.)
PhD Student at Stanford Intelligent Systems Lab.