iFM 2024 

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.

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.

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.

While ensuring the correctness of an implementation based on a formal functional specification provides the strongest guarantee, it can be prohibitively expensive to achieve. In practice, a combination of formal methods is commonly employed to attain an appropriate level of assurance. This includes static analyses to ensure the absence of runtime errors, deductive verification for functional correctness, and dynamic verification for components that cannot be proven through deductive verification. Frama-C is a source code analysis platform designed for the verification of large-scale programs written in ISO C source code. It offers comprehensive support for the integration of formal methods, offering users a set of plug-ins that facilitate static and dynamic analysis of safety-critical and security-critical software. Furthermore, the collaborative verification capabilities are achieved through the integration of these plug-ins on a shared kernel and their adherence to a standardized specification language known as ACSL (ANSI/ISO C Specification Language). This tutorial introduces Frama-C with a focus on the WP plug-in for deductive verification. We illustrate WP on several examples taken from Contiki, a lightweight operating system for the Internet of Things. (Slides (PDF), Exercises (zip file))