ETAPS Industry Day 2024


photo of David Delmas

David Delmas

Airbus Operations SAS

David Delmas has been working as an avionics software engineer at Airbus since 2001. He specializes in methods and tools, with a strong focus on formal verification. He has been contributing to the transfer of research prototypes into the toolset used by operational avionics software teams at Airbus. These tools include the Astrée and Fluctuat static analyzers, and the Frama-C platform. They are currently used as part of the verification processes of safety-critical avionics software products. He completed a PhD thesis on the static analysis of program portability by abstract interpretation in 2022.

Formal Verification of Avionics Software

The size and complexity of avionics software have grown exponentially from one aircraft generation to the next in the past 4 decades. Traditional software development processes leveraging informal verification techniques fail to scale within reasonable costs. In particular, verification is liable for a steadily growing share of the overall development costs. The 2015 current status was about 70%.

To address this issue, Airbus have been transforming internal development processes since 2016. Internal domain-specific languages have been developed to enable the formalization of design artifacts, and automate part of verification activities. Automation is enabled by the interoperation of tools relying on sound formal techniques. For instance, Frama-C/WP and SMT-solvers are used to automate unit verification with deductive methods. Most so-called Unit Proofs are automatic, assuming high-level memory and numerical models, as well as some preconditions. Such assumptions are verified by other tools, such as the Astrée static analyzer, which leverages Abstract Interpretation to prove the absence of run-time errors and check assumed non-aliasing properties. We rely on the CompCert formally verified compiler to enable that most formal verification activities may be conducted on source code.

Beyond safety properties and currently established processes, we also develop internally static analyses by Abstract Interpretation to automate regression verification and portability verification. In particular, our portability analysis is able to prove without false alarms the portability of low-level C avionics software up to 1 million lines of C across platforms with opposite byte-orders (endianness).

photo of Yannick Moy

Yannick Moy


Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

What Programmers Want from Proof with SPARK

SPARK is an industrial programming language with a unique focus on program proof, adopted in domains where software safety or security is paramount. Since a reboot in 2014, the language has known continuous evolution to match what programmers in these domains want: strong guarantees at reasonable cost. To accommodate different cost/benefit choices, we have defined a scale of levels of assurance that define different guarantees and their cost. SPARK supports these levels with dedicated features both in the programming language and in the analysis tool. We will present how these features match what programmers want, where they fall short today, and what we are working on to reduce that friction in the future.

photo of Fritz Henglein

Fritz Henglein

University of Copenhagen ( and Deon Digital (

Fritz Henglein is Professor of Programming Languages and Systems at DIKU, the Department of Computer Science at the University of Copenhagen, and Head of Research at Deon Digital, a Swiss-Danish technology company developing secure and scalable digital contract technology for both decentralized (blockchain, distributed ledger) and centralized systems. His research interests are in semantic, logical and algorithmic aspects of programming languages, high-performance functional programming, domain-specific languages, digital contracts, smart contracts and blockchain/distributed ledger systems, financial technology and various application domains.

From Theory to Practice: What is a contract, really?

Contracts are agreements between multiple parties that contain obligations, prohibitions and permission to exchange specified quantities of scarce resources under various conditions and within certain time limits. A financial contract, roughly speaking, is a money-now-for-money-later exchange. They are the backbone and organizing principle of companies interacting with each other. But what are they, beyond their renditions ranging from short emails and taped conversations to voluminous prospectuses and term sheets in stylized legal prose rendered in Microsoft Word? Can they be formalized, capturing their operational semantics, not only digitized as template text instantiated with data records?

In this subjective talk we sketch the history of digitizing and eventually digitalizing (formalizing) commercial and financial contracts; highlight their relation and difference, both significant, to process calculi; argue why Ethereum-style programs are neither smart nor contracts despite being called smart contracts; and describe our work on formalizing contracts as a domain-specific language as part of a ‘revolutionary’ approach to enterprise resource planning (ERP) systems and its 20-year journey to application, commercialization and deployment in multiple capital markets systems that bridge traditional regulated finance with fully automated and transparent real-time finance without traditionally obligatory intermediaries.

photo of Jan Peleska

Jan Peleska

University of Bremen and Verified Systems International

Since 1995, Dr. Peleska is professor for computer science at the University of Bremen. Before that, he worked with Philips and other companies as Senior Software Designer and later on as department manager in the field of cyber-physical systems. His research interests include formal methods for the development of safety-critical systems, test automation, and verification of deep neural networks. Industrial applications of his research focus on avionics and railway control systems. Jan Peleska is co-founder of Verified Systems International, a company dedicated to the development of tools and the provision of services in the field of safety-critical system development, verification, validation, and test. In 2015, Verified Systems International has been awarded the runner-up trophy of the European Innovation Radar Innovation prize for integrating novel test strategies with guaranteed fault detection capabilities into their test automation system RT-Tester.

Next Generation Model-based Testing for Industrial Applications

Model-based testing of safety-critical control systems has been a very active research field since the 1970s. A specialised branch of this field focused on the generation of so-called complete test suites. These guarantee a certain degree of fault coverage (e.g. language equivalence or property satisfaction), provided that certain hypotheses about the system under test are fulfilled. While having always been of high theoretical interest (black-box testing can really prove the absence of faults!), the practical applicability of complete test methods in industry has been successfully demonstrated within the last 15 years. Several companies - including Verified Systems - offer effective tool support for the model-based approach. It has to be admitted, however, that MBT tools have not become as successful as originally expected by researchers and tool providers. One of the root causes for this observation lies in the fact that ’typical’ software developers and testers prefer to program in C++, C#, Java, or Python to writing reference models in formalisms like UML, SysML, B, CSP and any other of the multitude of modelling formalisms advocated by the formal methods community. My own convictions about ’the best approach’ to test automation with guaranteed test strength, as well as the tool-oriented strategy of Verified Systems have therefore changed significantly within the last two years. (1) We are convinced that module-level testing should be performed by specifying properties and verifying them by means of test-based model learning in combination with model checking. (2) Integration testing and system-level testing should be performed by specifying system-level properties and an expert-driven, rule-based approach to create ‘meaningful’ end-to-end tests. (3) Guaranteed fault coverage should be the goal on module-level testing, while the higher levels rather require end-to-end tests that are ‘convincing’ for the certification authorities. In this presentation, I will focus on the first aspect (module testing) and demonstrate how the original ideas about ‘black-box checking’ by Peled, Vardi, and Yannakakis have been refined recently and made fit for industrial application. This is achieved by using more effective model learning techniques in combination with fuzz testing and monitors detecting the violation of safety properties. Moreover, static analysis techniques allow for the verification of hypotheses about the module under test, so that passing a test suite is really equivalent to a mathematical proof that the software correctly implements the required properties. Finally, a cloud-based tool platform allows for effective test suite creation, execution, and management of test-related artefacts.

photo of Leonardo Tonetto

Leonardo Tonetto


Leonardo is an Advisor on European R&D and Innovation.

European RD Projects: Participation and Opportunities

In this presentation, I will talk about different European funding opportunities for research and innovation projects. The main focus will be on Horizon Europe, EU’s flagship funding framework program, covering fundamental research all the way to market uptake. For that, I will introduce the fundamental structure of Horizon Europe and its eligibility, as well as details about upcoming topics in AI/ML and cybersecurity, where formal methods could be directly applied. With background in Computer Science, I currently work at Luxinnovation, the national innovation agency of Luxembourg, in the role of National Contact Point and Program Committee member on digital/ICT and cybersecurity topics.