Invited Speakers FMICS
Julia Badger
NASA Johnson Space Center, USAApplication of Formal Methods to Design and Verification of Autonomous Space Systems
As NASA's Artemis Program accelerates towards the Moon, the consideration of technologies needed for Martian exploration remains at the forefront. One significant technology gap is the ability to autonomously control complex, safety-critical, integrated spacecraft systems across the operational range of the vehicle and mission. The Gateway lunar space station has focused on autonomous spacecraft control as a major operational goal with the addition of a new software distributed hierarchical control architecture. This novel functionality depends strongly on correct behavior at every level of the architecture, and verification of this new system will require special consideration. Typical spacecraft testing campaigns rely on using similar hardware and software to run through mission use cases and limited edge cases. Given the distributed and autonomous nature of the Gateway software control system, alternative approaches are being explored to buy down risk in design, verification, and operation. For example, assume guarantee contracts were built into the design and will be used as part of spacecraft verification. Likewise, model checking will be leveraged during the operation of the autonomous spacecraft to understand spacecraft behavior given ground direction and commands. This talk will discuss the design, architecture, and plans for formal methods analysis of the Gateway.
Colin O'Halloran
Honourary Visiting Professor at the University of York, UK; CTO of D-RiSQ Ltd, UKReducing Time to Market through Formal Methods
Model Based Software Engineering (MBSE) integrates simulation, automation, and traceability into the development process. By using tools like Simulink and Stateflow developers can simulate system behaviour, automate code generation and maintain traceability from requirements to implementation. The major drawback with MBSE is showing not only that it does what is required, but much more importantly from a certification perspective, that it does not have unwanted functionality, including showing what happens when, not ‘if’ things go wrong. This challenge is caused by the semantics of the models being unclear, the link between the model and the requirements often being obscure and being able to show that code generated correctly implements the requirements for the model in an efficient and effective manner. The key is to leverage MBSE through evaluating verification artefacts generated by MBSE using Automated Reasoning. A key application of this approach to Robotic and Autonomous Systems is discussed in terms of commercial impact.
Bio
Colin has over 40 years of experience in high integrity systems, operating as a scientist, consultant and business group manager with RSRE, DERA and QinetiQ. He is an honourary Visiting Professor at the University of York and was previously a full professor of computer science at the University of Oxford. Colin is an internationally recognised expert in the validation and verification of software-based systems using formal methods. At RSRE he developed parts of the MALPAS analysis tool that was used in the assessment of the secondary protection system of the Sizewell B nuclear power station. Within DERA he was the technical authority for the development of the formal semantics of SPARK 83 carried out by PVL Ltd. Within QinetiQ he led the team that developed tools to mathematically verify the flight and engine control software for the Typhoon aircraft as well as the Auto-throttle and Auto-pilot. In 1996 he served on the European Space Agency’s Board of Inquiry into the very first launch of Ariane 5 and compiled those parts of the report concerning the software’s contribution to the failure. He carried out a survey of certification approaches on behalf of the Director of Helicopter projects following the Chinook crash on the Mull of Kintyre. Since 2012 Colin has been CTO of D-RiSQ Ltd that have developed automated formal methods based mathematical tools covering requirements capture and design verification, backed up by source code and object code verification.Joint CONFEST Invited Speakers
Ezio Bartocci
Professor at TU Wien, Vienna, Austria
Bio
Ezio Bartocci is a Full Professor at TU Wien and his work lies at the intersection of formal methods, quantitative reasoning, and AI-driven cyber-physical systems. He leads the Trustworthy Cyber-Physical Systems (TrustCPS) Research Group (https://trustcps.eu), where his research seeks to reconcile learning, autonomy, and uncertainty with formal methods, enabling cyber-physical systems that are not only intelligent, but also provably safe, energy-aware, and sustainable. His work is supported by a broad portfolio of competitive European, national, and industry-funded projects, in which he regularly serves as (co-)principal investigator, scientific coordinator, or work-package leader. He has contributed to numerous EU, FWF, FFG, WWTF, and industrial initiatives addressing quantitative verification, performance analysis under uncertainty and runtime monitoring. These projects span topics such as frequency-aware testing, probabilistic programming, reinforcement learning with normative guarantees, explainable AI, and trustworthy autonomous CPS, consistently bridging theory and practice by translating formal models into deployable methods for complex real-world systems. Prior to joining TU Wien, he was a Postdoctoral Researcher at Stony Brook University, where he worked on computational models of cardiac dynamics. This interdisciplinary experience continues to shape his view of cyber-physical systems as living, interacting entities, in which computation, physics, and learning co-exist. He joined TU Wien in 2012 and was promoted to Full Professor in 2020. Beyond his research contributions, Ezio Bartocci currently serves as Chair of the Doctoral College on Trustworthy Autonomous Cyber-Physical Systems, Vice-Chair of the Marie Skłodowska-Curie COFUND doctoral programme LogiCS@TU Wien, and Research Focus Coordinator for Computer Engineering at TU Wien. His work has received several distinctions, including Best Paper Awards at EMSOFT 2025, QEST 2022, and RV 2011, the Radhia Cousot Young Researcher Award 2022, and the EASST Best Software Science Award at ETAPS 2022.Ichiro Hasuo
Professor at the National Institute of Informatics (NII), Tokyo, Japan
