ETAPS Industry Day 2025

Keynotes

Chris Hobbs

BlackBerry QNX

Chris Hobbs was first challenged about the safety of the software system on which he was working in the late 1980s and has been interested in this area ever since. Most recently he has worked with BlackBerry QNX on the safety certification of its software and with QNX’s customers on robot surgeons, autonomous heavy trucks, medical devices, warehouse robots and other safety-critical systems. His particular interest is in applying formal methods to prove the correct operation of systems and predict emergent behaviour. He is a member of the SCSC Working Group on the Through-Life Assurance of Complex Systems and is the editor of the guidance being produced by that group. He is also a stakeholder in the UL4600 Technical Committee on autonomous systems and a Visiting Researcher at the University of Waterloo. He is the author of “Embedded Software Development for Safety-Critical Systems” (third edition), several aviation training books and a book on mathematical philosophy for young teenagers.

Weathering the Weather: The Storms Gathering Around the Development of Safety-Critical Systems

At least since the industrial revolution, we have been building systems that can hurt humans and the environment. We have assumed that a system becomes dangerous only when one of its components malfunctions, and have assessed its safety by analysing its failure rates. We now know that, in almost all dangerous situations, every component of the system behaved exactly as designed - nothing failed. This observation undermines the techniques traditionally used to justify that the system is adequately safe, and is just one of the many storms gathering around the design and development of such systems. Many current systems, particularly digital, socio-technical ones are “accidental”, exhibit unanticipated emergent behaviour and are encased in intellectual debt. This presentation describes some of these storms and asks how sufficient assurance can be obtained to allow a modern system to be deployed.

Rajeev Joshi

Amazon Web Services

Rajeev Joshi is a Principal Applied Scientist with the S3 Automated Reasoning Group at Amazon Web Services, where he leads a team applying formal methods to ensure the correctness of storage systems. His work focuses on developing scalable tools that continuously verify deep properties of large-scale production systems. Before joining AWS, Rajeev was Chief Engineer for Flight Software and Avionics Systems at NASA’s Jet Propulsion Laboratory (JPL). He was a member of the flight software team for the Mars rovers Curiosity and Perseverance, designing the spacecraft data management system and later serving as Data Management Chair after landing. His contributions at JPL earned him several awards, including two Mariner Awards and the NASA Exceptional Achievement Medal. Rajeev holds a B.Tech in Computer Science from IIT Bombay and an PhD from the University of Texas at Austin. He is an elected member and current chair of IFIP Working Group 2.3 on Programming Methodology.

Using lightweight formal methods to check correctness of production code for Amazon S3

I’ll present our experience applying lightweight formal methods to check correctness of key components within Amazon S3, the industry-leading cloud object storage service. Our “lightweight” approach enables seamless integration of formal models and tools into production pipelines where specifications and code are continuously evolving. We’ve been using our approach for over three years to check correctness of components at different layers of the software stack, from individual storage nodes to software running on an entire fleet of hosts. We check complex properties (such as serializability and crash consistency), using tools that run continuously in production pipelines, helping prevent numerous subtle bugs from reaching production. Notably, our framework has been adopted by engineers without formal methods expertise, allowing them to update specifications and develop tests to check new features and properties as S3 evolves. Our experience shows that formal methods can play a critical role in building confidence in the development of large-scale, mission-critical storage systems.

Tare Vatcher

Stellantis

Tara Vatcher is a highly accomplished Senior Technology Executive with a proven record of driving innovation and transformation. As President of LHP Software, she grew the organization from three employees to a $30 million annual revenue business in 12 years, establishing a world-class professional services team. At Stellantis, she led the reorganization of the powertrain controls and software division, streamlining processes and modernizing development practices. Now, serving as the Senior Vice President of Software Architecture and Development, she is building the software platform for Stellantis’ software-defined vehicles. With expertise in software development, engineering management, and cross-functional team leadership, Tara has consistently driven successful projects execution. Her knowledge spans embedded systems, agile methodologies, and process improvement. Recognized for her innovation and leadership, Tara has received multiple industry awards throughout her career. She holds a MBA from Indiana University’s Kelley School of Business.

The Challenge of Information Management within the Software Defined Vehicles

In a modern software development organization, one of the key metrics for success is the effective management and integration of design information throughout the development lifecycle. This is particularly challenging in the automotive domain, where the software development process is inherently complex and structured across distinct stages. These stages include requirements elicitation and definition, software architecture design, functional development, and multiple layers of virtual and on-target testing. Each stage operates as a specialized domain, employing unique tools and methodologies tailored to its specific objectives. Consequently, design information often becomes fragmented, confined to siloed domains and stored within specialized tools that lack transparency and accessibility across the broader organization. This fragmentation can hinder collaboration, reduce visibility, and compromise traceability. The critical challenge, therefore, is to establish a cohesive flow of information that seamlessly connects these domains. By creating a unified, transparent framework for information sharing and traceability, organizations can enable better collaboration, enhance decision-making, and ensure alignment across the entire software development process.

Thomas Chowdhury

MDA Space

Thomas Chowdhury is the Software Safety Lead for Canadarm3, a robotic system for the US-led Gateway that will enable sustainable human exploration of the Moon and Mars. Previously, he was also the Safety Lead for Autonomous train control at Thales Canada Inc. (now Hitachi). He also worked with Toyota on the Advanced Driver-Assisted System (ADAS) safety and cybersecurity certifications. He also worked with Sound Options Inc. to support FDA approval of their Tinnitus treatment. He completed his PhD at McMaster University focusing on safety critical systems and was a member of the McMaster Centre for Software Certification (McSCert). His research interests include assurance cases, safety, and cybersecurity certifications.

Safe Agile: A Safety Strategy for Agile Development Strategy for Spacecrafts or Space robots

A spacecraft or space robot is designed to fly and operate in outer space. Spacecrafts or space robots are used for a variety of purposes, including communications, Earth observation, meteorology, navigation, space colonization, planetary exploration, helping astronauts for space walk, relocate space modules etc. Software plays an important part in developing such complex safety critical systems. The Agile methodology is gaining popularity over traditional waterfall-style methodology because it produces ‘working’ software from the very beginning. To support safety critical software development for space domain, incremental safety analyses performed on incremental artefacts requires the elaboration of novel methodologies for complying with applicable safety standards. Safe Agile concept defines safety strategies for Agile development lifecycle for space domain.