A co-located workshop of the 64th IEEE Conference on Decision and Control (CDC 2025), Rio de Janeiro, Brazil, December 9-12, 2025. Registration information is available here, with an early registration deadline for this workshop set for September 3rd, 2025.

Organizers

• Abolfazl Lavaei (Newcastle University)

• Amy Nejati (Newcastle University)

• Kostas Margellos (University of Oxford)

• Antonis Papachristodoulou (University of Oxford)

Scope

Formal verification and controller synthesis for dynamical systems have garnered remarkable attention over the past two decades, driven by their extensive applications in safety-critical systems. These systems, whose failure can potentially result in severe consequences such as loss of life, injuries, or substantial financial losses, span wide-ranging domains, including aerospace, automotive, transportation systems, robotics, chemical processes, critical infrastructure, energy, and healthcare.

Given a property of interest for a dynamical model, formal verification is concerned to soundly check whether the desired specification is satisfied. If the underlying model is stochastic, the goal translates in formally quantifying the probability of satisfying the property of interest. A synthesis problem instead concerns dynamical models with the presence of control inputs: the goal is to formally design a controller (also known in different areas as policy, strategy, or scheduler), which is by and large a state-feedback architecture, to enforce the property of interest. This procedure is also called ‘‘correct-by-construction control design”, since every step in the controller synthesis procedure comes with a formal guarantee. In a stochastic setting, the key objective is to synthesize a controller that optimizes (e.g., maximizes) the probability of satisfying the given specification. As a result of their intrinsic soundness, formal methods approaches do not require any costly, exhaustive, and possibly unsuccessful post-facto validation, which is needed in many safety-critical, real-world applications.

While formal verification and controller synthesis have become indispensable across numerous applications, they often necessitate closed-form mathematical models of dynamical systems. However, these models might either be unavailable or too complex to be constructed in real-world scenarios. Consequently, one can often not employ model-based techniques to analyze and design complex dynamical systems. Hence, the use of data-driven techniques becomes essential in enabling formal analysis for systems with unknown dynamics.

Over the past decade, several data-driven techniques have been proposed for the formal verification and controller synthesis of unknown dynamical systems. One may classify them in two types: the indirect and direct approaches. More specifically, indirect data-driven techniques are those which leverage system identification to learn approximate models of unknown systems, followed by model-based controller analysis approaches. Their advantage is that once the identification phase is achieved, one may rely on the powerful armada of techniques available in model-based control. On the downside, most identification techniques are mainly limited to linear or some specific classes of nonlinear systems, and accordingly, acquiring an accurate model for complex systems via those indirect techniques could be complicated, time-consuming and expensive. In comparison, direct data-driven techniques are those that bypass the system identification phase and directly employ system measurements for the verification and controller design of unknown systems.

Objectives of the workshop

In this workshop, we bring together a number of researchers active in the area of data-driven verification and control with provable guarantees. The contributions will describe recently developed efforts towards new frontiers on the subject. Along with cherishing the exchange of ideas between researchers in the field, by gathering a number of key talks we aim to achieve the following goals for the audience attending the workshop:

• Provide to the researchers new to these topics an updated view of the state of the art on data-driven verification and control including indirect and direct data-driven techniques.

• Discuss scalable directions and areas to mitigate the, so-called, sample complexity.

• Suggest novel applications of these data-driven techniques.

Additionally, we hope the active discussions of the participants will lead to fruitful collaborations.

Workshop Program on December 9, 2025 (Local Time)

Speakers

• Speaker: Necmiye Ozay
  Affiliation: Associate Professor at University of Michigan, USA
  Title: Lifting as an Abstraction
  Abstract: For control synthesis for cyber-physical systems, it is common to create a discrete abstraction that satisfies a simulation relation with the original system. When working with discrete systems, going from a larger discrete system to a small one via abstraction simplifies the problem. However, when working with continuous systems one can also simplify the dynamics by lifting to a large dimensional (yet linear) system. This is in a sense similar to Kernel embeddings in machine learning. This talk will summarize some of our initial investigations in this direction, how such liftings can be used for synthesis of controllers, how it is related to Koopman embeddings, how such liftings can be learned and used in data-driven backward reachability analysis.
  Biography: Necmiye Ozay is the Chen-Luan Family Faculty Development Professor of Electrical and Computer Engineering, and an associate professor of Electrical Engineering and Computer Science and of Robotics at the University of Michigan, Ann Arbor. She received her PhD in Electrical Engineering from Northeastern University in 2010. After a postdoctoral position at Caltech in Computing and Mathematical Sciences, she joined Michigan in 2013. Her research interests include dynamical systems, control, optimization, and formal methods with applications in learning-enabled cyber-physical systems, system identification, verification and validation, and safe autonomy. She received the 1938E Award and a Henry Russel Award from the University of Michigan for her contributions to teaching and research. She received five young investigator awards, including NSF CAREER Award. She is also the recipient of the 2021 Antonio Ruberti Young Researcher Prize from the IEEE Control Systems Society for her fundamental contributions to the control and identification of hybrid and cyber-physical systems.

• Speaker: Peyman Mohajerin Esfahani
  Affiliation: Associate Professor at University of Toronto & TU Delft, Canada & The Netherlands
  Title: Inverse Optimization: An Efficient Learning Framework for Complex Behaviors
  Abstract: We study a class of learning models known as inverse optimization (IO), where the goal is to replicate the behaviors of a decision-maker (i.e., optimizer) with an unknown objective function. We discuss recent developments in IO concerning convex training losses and optimization algorithms. The main message of this talk is that IO is a rich learning model that can capture complex, potentially discontinuous behaviors, while the training phase is still a tractable convex program. We motivate the discussion with applications from control (learning the MPC control law), transportation (2021 Amazon Routing Problem Challenge), and robotics (comparing with state-of-the-art methods, including deep neural networks, in MuJoCo environments).
  Biography: Peyman Mohajerin Esfahani is an Associate Professor at the University of Toronto and Delft University of Technology. He joined TU Delft in October 2016, and prior to that, he held several research appointments at EPFL, ETH Zurich, and MIT between 2014 and 2016. He received the BSc and MSc degrees from Sharif University of Technology, Iran, and the PhD degree from ETH Zurich. He currently serves as an associate editor of Mathematical Programming, Operations Research, Transactions on Automatic Control, and Open Journal of Mathematical Optimization. He was one of the three finalists for the Young Researcher Prize in Continuous Optimization awarded by the Mathematical Optimization Society in 2016, and a recipient of the 2016 George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society. He received the ERC Starting Grant and the INFORMS Frederick W. Lanchester Prize in 2020. He is the recipient of the 2022 European Control Award.

• Speaker: Alessandro Astolfi
  Affiliation: Professor at Imperial College London, UK
  Title: Data-Driven Model Reduction with Provable Guarantees
  Abstract: This talk explores data-driven approaches to model reduction, with a particular focus on nonlinear moment matching theory. When approximating dynamical systems from input-output data, the goal is often not only to reduce the system's dimensionality but also to retain key physical characteristics. We will present recent advances in the construction of reduced-order models that achieve both objectives. Notably, these models can be developed solely from experimental data, without requiring explicit knowledge of the underlying system equations. We will demonstrate how the proposed methods provide theoretical guarantees on input-output properties such as passivity and finite gain.
  Biography: Alessandro Astolfi (IFAC Fellow, FIEEE) received the Laurea in Electronic Engineering from the University of Rome La Sapienza, Italy, in 1991; the M.Sc. degree in Information Theory and the Ph.D. degree with Medal of Honor with a thesis on discontinuous stabilization of holonomic systems from ETH-Zurich, Zurich, Switzerland, in 1995; and the Ph.D. degree for his work on nonlinear robust control from the University of Rome “La Sapienza,” Rome, in 1996.
  In 1992, he joined ETH-Zurich as a research associate. Since 1996, he has been with the Electrical and Electronic Engineering Department, Imperial College London, London, U.K., where he is currently Professor of Nonlinear Control Theory and College Consul for the Faculty of Engineering and Business School. From 2010 to 2022, he was the Head of the Control and Power Group at Imperial College London, and from 1998 to 2003, he was an Associate Professor with the Department of Electronics and Information, Politecnico of Milano, Milano, Italy. Since 2005, he has also been a Professor with the Dipartimento di Ingegneria Civile e Ingegneria Informatica, University of Rome Tor Vergata, Rome.
  His research interests include mathematical control theory and control applications, with special emphasis for the problems of discontinuous stabilization, robust and adaptive control, observer design, optimal control, game theory, and model reduction.
  Dr. Astolfi was the recipient of the IEEE CSS A. Ruberti Young Researcher Prize (2007); the IEEE RAS Googol Best New Application Paper Award (2009); the IEEE CSS George S. Axelby Outstanding Paper Award (2012); the Automatica Best Paper Award (2017); and the IEEE Transactions on Control Systems Technology Outstanding Paper Award (2023). He is a “Distinguished Member” of the IEEE CSS, IFAC Fellow, IET Fellow, and Member of the Academia Europaea. He is the recipient of the Institute of Measurement and Control Sir Harold Hartley Medal for “Outstanding contributions to the technology of measurement and control”.
  He was the Associate Editor, Senior Editor, Area Editor for several journals, and Editor-in-Chief for the European Journal of Control. He is Editor-in-Chief of the IEEE Transactions on Automatic Control (2018 –). He was Chair of the IEEE CSS Conference Editorial Board (2010–2017); Chair of the IEEE CSS Antonio Ruberti Young Researcher Prize (2015–2021); and Member of the IEEE Fellow Committee in 2016 and from 2019 to 2022. He is Vice Chair of the IFAC Technical Board (2020–2026); a Member of the IEEE Fellow N&A Committee; and a Member of the IEEE Thesaurus Editorial Board.

• Speaker: Abolfazl Lavaei
  Affiliation: Assistant Professor at Newcastle University, UK
  Title: Data-Driven Stochastic Control via Non-i.i.d. Trajectories: Foundations and Guarantees
  Abstract: In this talk, I will discuss how to advance data-driven trajectory-based methods for stochastic systems with unknown mathematical dynamics. In contrast to scenario-based methods that rely on independent and identically distributed (i.i.d.) trajectories, this talk adopts a data-driven framework where each trajectory is gathered over a finite horizon and exhibits temporal dependence—referred to as a non-i.i.d. trajectory. To ensure safety of dynamical systems using such trajectories, the current body of literature primarily considers unknown dynamics subject to bounded disturbances, which facilitates robust analysis. While promising, such bounds may be violated in practice and the resulting worst-case robust analysis tends to be overly conservative. To overcome these fundamental challenges, I consider stochastic systems with unknown mathematical dynamics, influenced by process noise with unknown distributions. In the proposed framework, data is collected from stochastic systems under multiple realizations within a finite-horizon experiment, where each realization generates a non-i.i.d. trajectory. Leveraging the concept of stochastic control barrier certificates constructed from data, I quantify probabilistic safety guarantees with a certified confidence level. To achieve this, the proposed conditions are formulated as sum-of-squares (SOS) optimization problems, relying solely on empirical average of the collected trajectories and statistical features of the process noise.
  Biography: Abolfazl Lavaei is an Assistant Professor in the School of Computing at Newcastle University, United Kingdom. Between January 2021 and July 2022, he was a Postdoctoral Associate in the Institute for Dynamic Systems and Control at ETH Zurich, Switzerland. He was also a Postdoctoral Researcher in the Department of Computer Science at LMU Munich, Germany, between November 2019 and January 2021. He received the Ph.D. degree in Electrical Engineering from the Technical University of Munich (TUM), Germany, in 2019. He obtained the M.Sc. degree in Aerospace Engineering with specialization in Flight Dynamics and Control from the University of Tehran (UT), Iran, in 2014. He is the recipient of several international awards in the acknowledgment of his work including Best Repeatability Prize (Finalist) at the ACM HSCC 2025, IFAC ADHS 2024, and IFAC ADHS 2021, HSCC Best Demo/Poster Awards 2022 and 2020, and IFAC Young Author Award Finalist 2019.

• Speaker: Antoine Girard
  Affiliation: Senior Researcher at Universit Paris-Saclay, CNRS, France
  Title: Safe Learning-based Nonlinear Model Predictive Control using Data-Driven Set-Valued Models
  Abstract: In this talk, we present a data-driven approach for optimization-based control of nonlinear systems with deterministic (i.e. non probabilistic) safety guarantees. In the first part of the presentation, we will present an approach for computing set-valued data-driven models that provably contains the dynamics of an unknown system. Starting with monotone systems, we present efficient algorithms for computing from data tight over-approximations of the unknown dynamics. We then show how the method can be extended to any nonlinear system with known bounds on first-order derivatives. In the second part of the talk, we show how these set-valued data-driven models can be used within a model predictive control scheme, enabling data-driven control with safety guarantees for a broad class of nonlinear systems. We finally show how the approach can be adapted to enable online learning.
  Biography: Antoine Girard is a Senior Researcher at CNRS and a member of the Laboratory of Signals and Systems. He is also an Adjunct Professor at CentraleSupélec, Université Paris-Saclay. He received the Ph.D. degree from Grenoble Institute of Technology, in 2004. From 2004 to 2006, he held postdoctoral positions at University of Pennsylvania and Université Grenoble-Alpes. From 2006 to 2015, he was an Assistant/Associate Professor at the Université Grenoble-Alpes. His main research interests deal with analysis and control of hybrid systems with an emphasis on computational approaches, formal methods and applications to cyber-physical and autonomous systems. Antoine Girard is an IEEE Fellow. In 2015, he was appointed as a junior member of the Institut Universitaire de France (IUF). In 2016, he was awarded an ERC Consolidator Grant. He received the George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society in 2009, the CNRS Bronze Medal in 2014, and the European Control Award in 2018.

• Speaker: Michelle Chong
  Affiliation: Assistant Professor at Eindhoven University of Technology, The Netherlands
  Title: A First Step Towards Cyber-Physical Systems Learning to be Secure
  Abstract: Cyber-physical systems (CPS) are the backbone of critical infrastructure today, such as utility systems delivering electricity, gas, water and sewage; to transportation networks. As we modernize existing infrastructure such as the electricity grid towards incorporating more forms of renewable energy sources, we introduce uncertainty to a large-scale system which can lead to undesirable behavior with existing algorithms. This is compounded by evolving threats such as cybersecurity, where the communication channels (cyber layer) that integrate the sensors, actuators and computation units (physical layer) are subject to manipulation with malicious intent. In this talk, we will present a data-driven method to identify the sensor(s) of a CPS that have been corrupted with potentially malicious intent. We leverage the celebrated Willem's fundamental lemma to handle uncertainty in the modeling, by first assuming that the system operator has access to offline data which are attack-free. We then show that the attack-free sensors can be identified online without the need for offline attack-free data for a class of replay and network delay attacks, respectively. This work presents a first step towards securing future cyber-physical systems.
  Biography: Michelle S. Chong is an Assistant Professor at the Department of Mechanical Engineering, Eindhoven University of Technology, the Netherlands. Michelle received the Bachelor of Engineering degree in Electrical Engineering, and the Ph.D. degree in mathematical control theory from the Department of Electrical and Electronic Engineering, the University of Melbourne, in 2008 and 2013, respectively. She has held postdoctoral positions at the University of California Santa Barbara, Lund University and KTH Royal Institute of Technology, Sweden. Since 2020, she is an Assistant Professor at the Department of Mechanical Engineering, TU Eindhoven, the Netherlands. Michelle was the 2013 recipient of the American Australian Association's postdoctoral fellowship, and won the best paper award at the 2016 ACM/IEEE 7th International Conference on Cyber-Physical Systems (ICCPS). Her research interests are the estimation and control of hybrid dynamical systems, with a special interest in the security and safety of cyber-physical systems.

• Speaker: Simone Garatti
  Affiliation: Associate Professor at Politecnico di Milano, Italy
  Title: Data-Driven Design with Formal Risk Guarantees via the Scenario Approach: A Sample Compression Framework
  Abstract: Recent years have witnessed a paradigm shift towards data-driven methods, which leverage observed data for design without requiring full knowledge of the underlying data generation processes. As automated decision-making systems increasingly operate without human supervision, ensuring the dependability of these methods has become critical. This calls for novel theoretical frameworks capable of providing a precise certification of the reliability of data-driven solutions. In this talk, recent advances in sample compression theory that lies at the heart of the so-called scenario approach are presented. When certain compression properties are satisfied, the theory enables unprecedented evaluations of the risk (i.e., the probability of underperforming on unseen data) associated with data-driven solutions. Moreover, algorithmic frameworks exist that can instill the desired compression properties into virtually any learning scheme, demonstrating that compression offers a framework of truly broad applicability. The presented results position the scenario approach as a comprehensive framework for data-driven design with formal risk guarantees and pave the way for the trustworthy deployment of data-driven techniques across a wide range of fields.
  Biography: Simone Garatti received both his M.S. and Ph.D. in Information Technology from the the Politecnico di Milano, Italy, in 2000 and 2004, respectively. After graduating, he joined the Faculty of the Politecnico di Milano, where he currently holds a position of Associate Professor in the Automatic Control area at the Dipartimento di Elettronica, Informazione e Bioingegneria. He also held visiting positions at some prestigious foreign universities, like the University of California San Diego (UCSD) (as winner of a fellowship for the short-term mobility of researchers from the National Research Council of Italy), the Massachusetts Institute of Technology (MIT), and the University of Oxford. From 2013 to 2019 he served for the EUCA Conference Editorial Board, while he is currently member of the IEEE-CSS Conference Editorial Board and Associate Editor for the International Journal of Adaptive Control and Signal Processing and for the Machine Learning and Knowledge Extraction journal. In 2024, he served as tutorial chair of the 6th Learning for Dynamics and Control conference (L4DC 2024), while in 2011 he was publicity co-chair for the 18th IFAC World Congress. Simone Garatti has pioneered with co-authors the theory of the scenario approach, a unitary framework to make designs where the effect of uncertainty is controlled by knowledge drawn from past experience, and in recognition of his contributions he was keynote speaker in the IEEE 3rd Conference on Norbert Wiener in the 21st Century in 2021, he gave a semi-plenary address in the 2022 European Conference on Stochastic Optimization and Computational Management Science (ECSO-CMS), and in 2024 was invited speaker at the AAAI Workshop on Learnable Optimization (within the 38th Annual AAAI Conference on Artificial Intelligence). Simone Garatti is the author/co-author of the book “Introduction to the Scenario Approach” published by SIAM in 2018 and of more than 100 contributions in international journals, international books, and proceedings of international conferences. Besides data-driven optimization and decision-making, his research interests also include system identification, uncertainty quantification, and machine learning.

• Speaker: Ryan K. Cosner
  Affiliation: Assistant Professor at Tufts University, USA
  Title: Safe Autonomy for Real-World Robotics
  Abstract: Robots can only achieve safe, lifelong autonomy if they can navigate the complex, stochastic uncertainties of the real world. Moreover, these systems must be able to make risk-aware decisions with limited data, sensing, and computational resources. In this talk, I discuss how I use tools from nonlinear control theory, machine learning, and robotics to achieve this goal. In particular, I consider control barrier functions (CBFs) as a method for ensuring safety and propose techniques that extend their guarantees to real-world systems. I first discuss my contributions to the traditional deterministic safety paradigm, which relies on worst-case, adversarial assumptions on uncertainty. Next, I present my work on an alternative stochastic, risk-sensitive paradigm that allows control algorithms to intelligently manage the system’s level of risk. To further improve a system’s ability to navigate the real-world, I demonstrate how machine learning can improve upon theoretical models using episodic supervised learning, self-supervised learning, and generative modeling in data-sparse settings. To verify the utility of these methods and the validity of their theoretical guarantees, I deploy them on a variety of bipedal, quadrupedal, wheeled, and flying robot platforms.
  Biography: Ryan K. Cosner received his Ph.D. in mechanical engineering from the California Institute of Technology (Caltech) in 2025. He earned his M.S. from Caltech in 2021 and B.S. from the University of California, Berkeley in 2019. In 2022, he interned with the Autonomous Vehicle Research Group at NVIDIA. He is currently the Glenn R. Stevens Assistant Professor of mechanical engineering at Tufts University, Medford, MA, USA. His main research interests include nonlinear control and machine learning with applications to dynamic, risk-aware safety-critical robotics.