About PhD School

The ICTAC Postgraduate School on Formal Methods for Building Mission-Critical Systems will be held at the NH Bariloche Edelweiss Hotel, Argentina, on November 9–10, 2026. It targets master’s and Ph.D. students, early-stage researchers, and lecturers in computer science and mathematics. The school offers specialized training in formal methodologies for developing critical software, particularly for the satellite, aerospace, automotive, and nuclear sectors. The program consists of tutorials (two 2-hour lectures) and short talks (1 hour) by leading experts in the area.

Lecturers

Dr. Mariëlle Stoelinga

Dr. Marielle Stoelinga

University of Twente

Mariëlle Stoelinga is Professor of Risk Management for high-tech systems at the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. In addition, she has a part-time position at the Software Science department of Radboud University Nijmegen. She is also programme manager for the executive master’s programme Risk Management, in which professionals are trained to be professional risk managers.

Predictive maintenance through the lens of complexity science.

First, I will provide a concise introduction to the principles and applications of risk management in engineering and industrial contexts. It outlines key concepts such as hazard identification, risk assessment, and decision-making under uncertainty. A central focus is Fault Tree Analysis (FTA), a systematic, top-down method for analyzing the causes of system failures. Second, I will talk about predictive maintenance is an innovative technique that provides efficient solutions in reliability engineering: By predicting failures (either by AI & data, or physical models or their combination) , inefficient maintenance can prevent these failures before they occur. While predictive maintenance is successful for components, scaling up to system-level is a major challenge. Here is where complexity science comes in, i.e. the study of complex systems (e.g. cities, companies, the human brain) across fields, like biology, urban planning, physics, and economics. In this field, agent-based models play a prominent role: large simulation models to understand how component behavior leads to system level properties.

Dr. Sebastian Uchitel

Dr. Sebastian Uchitel

University of Buenos Aires - CONICET

Sebastian Uchitel is a Professor at Universidad de Buenos Aires, Principal Investigator at CONICET-Argentina, holds a Readership at Imperial College London. and is an affiliated researcher at Universidad de San Andrés, Argentina. His research interests are in behaviour modelling, analysis and synthesis applied to requirements engineering, software architecture and design, and in particular the use of synthesis at runtime to support system adaptation. He was Editor-in-Chief of the IEEE Transactions on Software Engineering and has served in editorial boards for CACM, REJ, and SCP.. He was program co-chair of ASE’06 and ICSE’10, and General Chair of ICSE’17. He has served on the board of directors of the Argentine national oil company, YPF, and held advisory roles to the Argentine government. He is a member of the Argentine National Academy of Exact, Physical and Natural Sciences.

Discrete Event Control for System Adaptation

Automated construction of correct operational strategies to control a reactive (and possibly distributed) system in such a way that certain system-goals are guaranteed has been studied for several decades. In this course I will introduce one approach to controller synthesis, discrete event control and discuss its differences with some of related approaches such as reactive synthesis and AI planning. I will then cover some of the additional difficulties (and challenges) that arise when these controllers are actually deployed in cyber-physical systems, including guaranteeing end-to-end correctness, hybrid enactment architectures, and dynamic revision and deployment of controllers.

Dr. César Sánchez

Dr. César Sanchez

IMDEA Software Institute

Cesar Sanchez is full (research) professor at the IMDEA Software Institute in Madrid, Spain. He holds a PhD from Stanford University in 2007. He was a postdoc at University of California Santa Cruz before joining the IMDEA Software Institute in 2008. His current research focuses on applications of logic to computer science and in formal methods for reactive systems, and in particular temporal logics for hyperproperties and runtime verification. His main practical interests are applications of runtime verification to autonomous systems and blockchain and smart-contract reliability.

TBA

Tutorials

Two 1-hour sessions led by distinguished experts. Speakers and topics: To be announced.