Welcome to iFM 2024!

The 19th International Conference on Integrated Formal Methods (iFM) will take place on 13–15 November 2024 at the University of Manchester, UK, with co-located workshops scheduled for 11–13 November 2024.

News & Updates

Invited Speakers

Proof for Industrial Systems using Neural Certificates
Amazon Web Services and Magdalen College, Oxford, UK
Abstract

We introduce a novel approach to model checking software and hardware that combines machine learning and symbolic reasoning by using neural networks as formal proof certificates. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates and the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure is entirely unsupervised, formally sound, and practically effective. We implemented a prototype and compared the performance of our method with the state-of-the-art academic and commercial model checkers on a set of Java programs and hardware designs written in SystemVerilog.

Daniel Kröning
Daniel Kröning
Biography

Daniel Kröning is a Senior Principal Applied Scientist at Amazon, where he works on the correctness of the Neuron Compiler for distributed training and inference. Prior to joining Amazon, he worked as a Professor of Computer Science at the University of Oxford and is the co-founder of Diffblue Ltd., a University spinout that develops AI that targets code and code-like artefacts.

He has received the Semiconductor Research Corporation (SRC) Inventor Recognition Award, an IBM Faculty Award, a Microsoft Research SEIF Award, and the Wolfson Research Merit Award. He serves on the CAV steering committee and was co-chair of FLOC 2018, EiC of Springer FMSD, and is co-author of the textbooks on Decision Procedures and Model Checking.

Compositional Symbolic Execution for Over-approximating and Under-approximating Reasoning
Imperial College London, UK
Abstract

A relatively recent challenge has been to develop symbolic-execution techniques and tools that are functionally compositional with simple function specifications that can be used in broader calling contexts. The technical break-through came with the introduction of separation logics for reasoning about partial mutable state, leading to compositional symbolic execution tools being developed in academia and industry. Many of these tools have been grounded on a formal foundation, but either the function specifications are validated with respect to the underlying symbolic semantics of the engine, with no meaning outside the tool, or there is a large gulf between the theory and the implementations of the tools. In this talk, I will introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce functions for updating the symbolic state when calling function specifications, a technique used by VeriFast, Viper and Gillian but not previously characterised independently of the tool. A surprising property is that our semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this insight to extend the Gillian platform with incorrectness reasoning, developing automatic true bug-finding using incorrectness bi-abduction, which our engine incorporates by creating fixes from missing-resource errors. We have shown that the Gillian implementation of the consumer and producer functions satisfy the properties described by our axiomatic interface, and evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool to support both correctness and incorrectness reasoning, as well as being grounded on a common formal compositional symbolic execution engine.

This talk is loosely based on the paper “Compositional Symbolic Execution for Over-approximating and Under-approximating Reasoning” by Andreas Lööw, Daniele Nantes Sobrinho, Sacha-Elie Ayoun, Caroline Cronjäger, Petar Maksimović and Philippa Gardner, ECOOP 2024, distinguished paper.

Philippa Gardner
Philippa Gardner
Biography

Philippa Gardner is a professor in the Department of Computing at Imperial College London and has a UK Research and Innovation Established Fellowship from 2018–2023. Her research focusses on program specification and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction.

A Formal Approach to Railways Interlocking Design
Fondazione Bruno Kessler, Italy
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.

Alessandro Cimatti
Alessandro Cimatti
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 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, Cimatti 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 been the leader of several technology transfer projects, including research projects funded by the European Union, the European Space Agency and the European Railway Agency, as well as of industrial collaborations with RFI, SAIPEM and Boeing.