Alessandro Cimatti (Fondazione Bruno Kessler)
Biography: Alessandro Cimatti is the Director of the Center for Digital Industry at Fondazione Bruno Kessler in Trento, Italy. His research interests include formal verification, model checking, temporal logics, runtime verification, safety assessment, diagnosis and planning. Cimatti has authored more than 250 papers in the fields of formal methods and artificial intelligence. For his fundamental works on Bounded Model Checking and on Satisfiability Modulo Theories, he has received the TACAS 2014 Most Influential Paper award, the ETAPS 2017 Test of Time award and the CAV Award in 2018 and 2021. He has led numerous technology transfer projects, including research initiatives funded by the European Union, the European Space Agency and the European Railway Agency, as well as industrial collaborations with RFI, SAIPEM, Bosch and Boeing.
Title: The OPERA Framework: Formal Design of Railways Interlocking Systems
Abstract: Many railways interlocking systems are still based on electromechanical solutions. They are hard to understand and costly to modify, and can be considered legacy systems. In this talk I will present the research underlying a novel process for the development of interlocking applications. The proposed methodology is able on one side to analyze and reverse-engineer legacy relay-based interlocking systems, and on the other to support the specification and verification of interlocking procedures by means of a model-based approach. Research challenges include modeling and verification of continuous-time, real-valued transition systems, automated abstraction for reverse engineering and specification mining, automated test generation, and parameterized verification.
Jun Sun (Singapore Management University)
Biography: Jun Sun is a Professor at Singapore Management University (SMU). He earned his Bachelor’s and Ph.D. degrees in Computer Science from the National University of Singapore (NUS) in 2002 and 2006, respectively, and has been a faculty member since 2010. Professor Sun’s research interests span AI safety, software engineering, formal methods, and more. He is passionate about designing algorithms to solve challenging real-world problems and is equally devoted to enjoying life. His work has been recognized with ACM Distinguished Paper Awards multiple times, and he serves as a technical consultant for multiple companies. For more information, please visit his website: https://sunjun.site.
Title: Building Trustworthy AI Agents: Challenges and Attempts
Abstract: Large language models and AI agents are advancing at an extraordinary pace, exhibiting increasingly sophisticated capabilities in reasoning, planning, and autonomous decision-making. Yet, these advances are accompanied by growing safety and security concerns, particularly as such systems move toward deployment in high-stakes and safety-critical settings. Ensuring their reliability is therefore no longer optional—it is a fundamental requirement. In this talk, I will examine the challenge of developing systematic approaches to AI safety, and present three complementary families of techniques for improving the safety and trustworthiness of large-scale AI systems. For each, I will highlight key open theoretical problems and discuss emerging research efforts that begin to address them.
Alessandro Abate (University of Oxford)
Biography: Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor TU Delft. He received a PhD and MSc degrees from UC Berkeley and the University of Padua.
Title: Neural Proofs for Sound Verification of Complex Programs and Systems
Abstract: I discuss the construction of sound proofs for the formal verification and control of complex models, encompassing broad classes of (probabilistic) reactive programs and (stochastic) dynamical systems.
Neural proofs comprise two parts. Firstly, proof rules encode formal requirements ensuring the verification of general temporal specifications over the models of interest. Then, certificates can be constructed from said proof rules: we leverage an inductive approach, which accesses samples generated from the model's dynamics, trains neural nets, whilst generalising them via SAT-modulo-theory queries, based on the full knowledge of the models.
In the context of sequential decision making problems, I also discuss how to additionally generate policies/strategies/controllers, in order to formally attain general temporal specifications.
Michael Butler (University of Southampton)
Biography: Michael Butler is a Professor of Computer Science and Dean of Engineering and Physical Sciences at the University of Southampton, UK. He works in the area of mathematical methods for design and verification of safe and secure software-based systems, specialising in model-based formal methods, in particular Event-B. His research work encompasses applications, tools and methodology for formal methods. He has made key theoretical and methodological contributions to the Event-B formal method that enable it to scale to large complex systems. These contributions enable modular analysis in terms of how systems models are structured and analysed as well as methods for development of domain-specific mathematical theories that are reusable across multiple projects.
Title: Abstraction and Refinement for Modelling and Analysis in Cyber Physical System Design
Abstract: Recent ideas on guaranteed safe AI from leading formal methods researchers propose the use of three components to ensure safe AI systems: a safety specification, a world model, and a verifier. At a high level this represents a systems approach to safety analysis which aligns well with common usage of abstraction/refinement formal methods, such as Event-B. Constructing specifications and world (or environment) models for complex systems remains challenging, and abstraction and refinement approaches are aimed at addressing system complexity through incremental modelling and verification. We outline the role of abstraction, system invariants, and refinement in supporting a systematic approach to world modelling and hazard analysis for cyber physical systems. Increasing levels of autonomy being deployed in robotic systems means weaker concepts of control and predictability, increasing risk of accidents, and challenging conventional hazard analysis methods. The role of formal methods, such as Event-B, is quite well established for traditional safety-critical systems, but it remains an open question whether and how such methods are applicable to systems with autonomy and learning-based control. We also explore this open question.