0728, 16:30–18:30 (UTC), BoF/Mini Track
This minisymposium presents modern approaches to analyze a variety of mathematical systems in Julia, via set propagation techniques: dynamical systems, cyberphysical systems, probabilistic systems, and neural networks. To deploy those systems in the real world there is an increasing demand for safe and reliable models. The speakers represent a broad crosssection of work from different fields that build on setbased techniques and global optimization to address such challenges.

Organisers: Marcelo Forets (@mforets) and Christian Schilling (@schillic)

Moderator: David P. Sanders (@dpsanders)
A new generation of algorithms is addressing the fundamental challenge of how to exhaustively explore all possible scenarios for simulation of dynamical systems under model uncertainties. Moreover, deep neural networks play an increasing role in control and safetycritical applications, although it is often not known how to guarantee that they will behave correctly and safely under all circumstances. This minisymposium will host applications of setbased techniques and global optimization in Julia that address these questions.
We have made sure to reach out to several different groups who are working on set propagation techniques and their application in a wide range of areas, to present a broad overview of the area.
Plan: 1 introductory talk (nonJuliaspecific), 5 regular talks, 1 Q&A panel.

Introduction by Goran Frehse (Hybrid Systems Semantics group, Computer Science and System Engineering Laboratory (U2IS), ENSTA Paris. Homepage.

Using Set Propagation and the Finite Element Method For Time Integration in Transient Solid Mechanics Problems. By Jorge Pérez Zerpa (speaker), Marcelo Forets and Daniel Freire Caporale. The Finite Element Method (FEM) is the gold standard for numerical simulation in transient solid mechanics problems. Several timeintegration algorithms have been developed in recent decades; however, it is still a challenging problem to completely describe the family of dynamicallyfeasible behaviors from given sets of initial states. In this talk we take a setbased approach and conclude that it has a lot of potential to efficiently solve such problems.

Dionysos.jl: Optimal Control of CyberPhysical Systems. By Benoit Legat, Guillaume Berger, Julien Calbert (speaker) and Raphaël Jungers. Dionysos.jl is software produced by the ERC project Learning to Control (L2C). In view of the CyberPhysical Systems (CPS) revolution, the only sensible way of controlling these complex systems is by discretizing the different variables, thus transforming the model into a simple combinatorial problem on a finitestate automaton, called an abstraction of this system. Our goal is to transform this approach into an effective, scalable, cuttingedge technology that will address the challenges of CPS and unlock their potential.

Solving Optimization Problems with Embedded Dynamical Systems. By Matthew Wilhelm (speaker) and Matthew Stuber. We will discuss our recent work at PSORLab: EAGODynamicOptimizer.jl and DynamicBounds.jl packages. These extend our EAGO.jl nonconvex optimizer to address formulations containing embedded dynamical systems. We highlight a series of approaches for constructing the requisite convex and concave relaxations of differential equations in the original decision space and discuss the use of such techniques in a global optimization context. These methods may readily be composed with existing McCormick relaxation approaches, which allows for the solution of general nonlinear formulations to certified global optimality. Use cases relevant to hybrid datadriven process modeling, parameter estimation, and worstcase robust design are discussed.

Computing with sets of probabilities in Julia. By Ander Gray. There are many ways to mathematically define a set of probability distributions, including: intervals, possibility distributions, random sets and probability boxes (pboxes). These structures were discovered independently from one another, but are often synonymous and can be translated. Imprecise Probability theory links all these theories into one. In this presentation, we present ProbabilityBoundsAnalysis.jl (PBA) a numerical implementation of pbox arithmetic in Julia, which gives an arithmetic of random variables where both marginal distributions and dependencies may be partially defined. We show how PBA may be used to rigorously propagate distributions and pboxes in reachability problems using ReachabilityAnalysis.jl.

Methods to Soundly Verify Deep Neural Networks. By Tomer Arnon. Deep neural networks are widely used for nonlinear function approximation, with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain inputoutput properties. NeuralVerification.jl implements several methods that have emerged recently for soundly verifying such properties. We discuss fundamental differences between existing algorithms and compare them on a set of benchmark problems.
Professor of Computational Science at the Universidad Nacional Autónoma de México and visiting professor at MIT.
Interested in computational science, interval arithmetic, and numericsymbolic computing.
Author of the JuliaIntervals suite of packages for interval arithmetic, and various tutorials on Julia.
 Calculating a million stationary points in a second on the GPU
 Global constrained nonlinear optimisation with interval methods
 Solving discrete problems via Boolean satisfiability with Julia
 Open and interactive Computational Thinking with Julia and Pluto
 Publish your research code: The Journal of Open Source Software
 Introduction to metaprogramming in Julia
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 postdoc 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 cyberphysical 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 machinelearned components. He is a colead developer in the JuliaReach ecosystem.
Ander Gray received an MSci in Physics from Queen’s University Belfast (2017). Since then, he has been a PhD student at the University of Liverpool and Culham Centre for Fusion Energy, studying Uncertainty Quantification. For his thesis work, Ander researches methods for efficiently propagating uncertainty in radiation transport simulations. He is also involved in developing methods and software for calibrating and propagating uncertainties through computational models, in the form of imprecise probabilities.
Matthew E. Wilhelm received a B.S. in Applied Mathematics from the University of North Carolina at Greensboro, Greensboro, NC, USA (2009), and a M.S. in Chemical Engineering from Columbia University, New York, NY, USA (2011). He is currently a PhD Candidate in Chemical and Biomolecular Engineering at the University of Connecticut where his research interests include: nonconvex optimization, dynamic simulation and optimization, mathematical biology, and engineering & STEM pedagogy.
Jorge Pérez Zerpa obtained a Doctorate in Engineering degree by Universidad de la República in Uruguay, a MSc in Mechanical Engineering degree by Universidade Federal de Rio de Janeiro in Brazil, and did a stage at INRIA's TAO team in France. He is Assistant Professor at the Structures Department of the School of Engineering in Universidad de la República, and Researcher level 1 at ANII.uy . His research work includes the development and application of numerical methods in computational modelling of solids and structures, with focus in constitutive parameter identification methods. He leads the development of the Open Nonlinear Structural Analysis Solver (onsas.org) based in the application of the Finite Element Method.
Goran Frehse has a Diploma in Electrical Engineering and Information Technology from Karlsruhe Institute of Technology, Germany, and a PhD in Computer Science from Radboud University Nijmegen, the Netherlands. From 2006 to 2018, he was an associate professor at the University Grenoble Alpes, from which he obtained a habilitation in 2016. From 2016 to 2018, he held a research chair (Chaire Initiative Universitaire Alpes) at the Univ. Grenoble Alpes. Since 2018, he is a professor at ENSTA Paris, where he continues his research on safe cyberphysical systems.
Ph.D. candidate at the Institute of Information and Communication Technologies, Electronics and Applied Mathematics (ICTEAM) of Université Catholique de Louvain (UCL), LouvainlaNeuve, Belgium.
Ph.D. candidate at the Stanford Intelligent Systems Laboratory, Stanford (USA).