AE Seminar

 

 

A Correct-by-Construction Paradigm 
for Designing Autonomous Systems

 

ft. 

 

Majid Zamani

Associate Professor | Associate Chair for Graduate Education | Department of Computer Science
University of Colorado, Boulder

 

Tuesday, March 11
11 am - 12 pm
Weber SST III, 1 Classroom

 

 

About the Seminar: 
Correct-by-construction synthesis is at the forefront of integrating formal methods with control theory, particularly in the design of safety-critical systems. This approach moves beyond the traditional iterative cycle of redesign, verification, and validation, advocating for a more streamlined methodology that guarantees formal requirement satisfaction through rigorous proofs. By embedding closed-loop system correctness directly into the design stage, it ensures correctness from the outset. Over the past two decades, significant progress has expanded the applicability of correct-by-construction synthesis, particularly for cyber-physical systems that intricately combine discrete control logic with continuous dynamics. Advances in symbolic techniques, state-space reduction strategies, and compositional reasoning have enhanced the feasibility of applying these principles to highly complex autonomous systems. Additionally, recent research has explored novel directions, such as leveraging barrier certificates and data-driven methods, which are especially useful when system models are incomplete or unavailable. This talk will highlight our latest breakthroughs in establishing a solid foundation for the correct-by-construction synthesis of cyber-physical systems. If time permits, we will also explore our ongoing efforts in secure-by-construction synthesis, which seeks to integrate safety and security requirements seamlessly into the system design process.

 

About the Speaker: 
Majid Zamani is an Associate Professor in the Computer Science Department at the University of Colorado Boulder. From May 2014 to January 2019, he was an Assistant Professor in the Department of Electrical Engineering at the Technical University of Munich. He holds a Ph.D. in Electrical Engineering and an M.A. in Mathematics from the University of California, Los Angeles (UCLA) (2012), an M.Sc. in Electrical Engineering from Sharif University of Technology (2007), and a B.Sc. in Electrical Engineering from Isfahan University of Technology (2005). Dr. Zamani’s contributions to control theory and cyber-physical systems have been recognized with several awards, including the George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society (2023), the NSF CAREER Award (2022), and both an ERC Starting Grant (2018) and an ERC Proof of Concept Grant (2023) from the European Research Council. He has served as Program Chair and General Chair for various conferences and workshops in control theory and formal methods, including Numerical Software Verification (NSV) and IFAC Conference on Analysis and Design of Hybrid Systems (ADHS). He is currently a steering committee member for ADHS, the Chair of the IEEE Technical Committee on Hybrid Systems, and an Associate Editor for both the IEEE Transactions on Automatic Control and Discrete Event Dynamic Systems.