2021-07-26 –, Green
JuliaReach is among the best-of-breed software addressing the fundamental problem of reachability analysis: computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. We explain the role of Julia's multiple dispatch to gain an unprecedented level of flexibility and expressiveness in this area. We explore diverse applications including differential equations, hybrid systems and neural network controlled systems.
We present JuliaReach, a Julia ecosystem to perform reachability analysis of dynamical systems. JuliaReach builds on sound scientific approaches and was, in two occasions (2018 and 2020) the winner of the annual friendly competition on Applied Verification for Continuous and Hybrid Systems (ARCH-COMP).
The workshop consists of three parts (respectively packages) in JuliaReach: our core package for set representations, our main package for reachability analysis, and a new package applying reachability analysis with potential use in domain of control, robotics and autonomous systems.
In the first part we present LazySets.jl, which provides ways to symbolically represent sets of points as geometric shapes, with a special focus on convex sets and polyhedral approximations. LazySets.jl provides methods to apply common set operations, convert between different set representations, and efficiently compute with sets in high dimensions.
In the second part we present ReachabilityAnalysis.jl, which provides tools to approximate the set of reachable states of systems with both continuous and mixed discrete-continuous dynamics, also known as hybrid systems. It implements conservative discretization and set-propagation techniques at the state-of-the-art.
In the third part we present NeuralNetworkAnalysis.jl, which is an application of ReachabilityAnalysis.jl to analyze dynamical systems that are controlled by neural networks. This package can be used to validate or invalidate specifications, for instance about the safety of such systems.
Meet the team of researchers and students that form the JuliaReach network:
-
Luis Benet. Universidad Nacional Autónoma de México. Validated integration, Nonlinear Physics. He is also one of the lead developers of JuliaIntervals.
-
Marcelo Forets. Universidad de la República, Uruguay. Reachability Analysis, Hybrid Systems, Neural Network Robustness.
-
Daniel Freire Caporale. Universidad de la República, Uruguay. Reachability, PDEs, Fluid Mechanics.
-
Sebastian Guadalupe. Universidad de la República, Uruguay. Julia Seasons of Contributions 2020 Alumni. Mathematical Modeling, Hybrid systems.
-
Uziel Linares. Universidad Nacional Autónoma de México. Google Summer of Code 2020 Alumni. Nonlinear reachability, Taylor models.
-
Jorge Pérez Zerpa. Universidad de la República, Uruguay. Finite Element Method, Structural Engineering, Material Identification.
-
David P. Sanders. Universidad Nacional Autónoma de México and visiting professor at MIT. Computational Science, Interval Arithmetic, and Numeric-symbolic Computing. He is also one of the lead developers of JuliaIntervals.
-
Christian Schilling. University of Konstanz, Germany. Formal Verification, Artificial Intelligence, Cyber-Physical Systems.
Marcelo Forets is an Applied Mathematician that works as Assistant Professor at Universidad de la República (Uruguay). Born in Uruguay (Montevideo, 1988), he graduated in Physics and in Electrical Engineering, then moved to France for a PhD in Mathematics and Informatics (Univ. Joseph Fourier, France) on the quantum random walk, a model of particular interest to Quantum Computing. He was a post-doc researcher at VERIMAG laboratory of Université Grenoble Alpes (France) under the supervision of Oded Maler and Goran Frehse, where he started to develop what is now the JuliaReach package ecosystem. His research has to do with developing innovative numerical tools that impact decisions regarding reliability, correctness and safety of control systems, hybrid dynamical systems, and robustness analysis of neural networks.
Christian Schilling received his Ph.D. degree in computer science from the University of Freiburg, Germany, in 2018 under the supervision of Andreas Podelski. He was a postdoctoral research fellow at IST Austria in the group of Thomas A. Henzinger. Since 2020 he is the interim professor for cyber-physical system at the University of Konstanz, Germany. Christian's research in the area of formal methods is focused on the analysis, verification, and synthesis of systems with dynamical or machine-learned components. He is a co-lead developer in the JuliaReach ecosystem.