Month: July 2025

Introducing Separation Logic into ACSL
Frama-C/WP is a tool implementing deductive verification on C programs annotated by properties in the ACSL language. Both WP & ACSL rely on classical Hoare Program Logic, which is known to be intrinsically limited, especially for programs with complex structures using pointers. The modern approach to deal with such programs is to use Separation Logic instead, which is more powerful than Hoare Logic, but is more difficult to use in practice, and for which there is no support from main stream automated provers, typically SMT solvers like Z3, Alt-Ergo, CVC4 or CVC5. In this talk, I would present the directions we are investigating for introducing (some ingredients from) Separation Logic into ACSL and Frama-C/WP.

Towards a formalization and generalization of divide-and-conquer parallel design pattern
Structuring is essential in parallel programming, as it helps manage the inherent complexity of concurrent computation. One effective way to achieve such structuring is through programming patterns and algorithmic skeletons. Among these, the divide-and-conquer pattern plays a fundamental role. It is defined by a recurrence relation that expresses the solution to a problem in terms of the solutions to smaller subproblems of the same nature. This pattern supports a wide range of computational scenarios, making it valuable to develop a general specification that captures all its possible forms and use cases. We aim to demonstrate that the divide-and-conquer pattern can be generalized in such a way that it subsumes many other parallel programming patterns. To support this claim, we propose a formal and comprehensive formulation of the divide-and-conquer paradigm. Such a generalization can serve not only theoretical purposes but also practical ones—particularly in the design of parallel programming libraries and APIs that rely on divide-and-conquer-based skeletons.

Frama-C/Eva: a concrete application of abstract interpretation
André Maroneze (CEA LIST)
July 16, 2025
The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows automatic identification of several kinds of undefined behaviors. It can be seen as an “abstract debugger”, and help understand what the code does. With some experience, it can scale up to 100k’s lines of code. This presentation will focus on practical examples, some theoretical foundations, and ongoing challenges concerning the application of abstract interpretation to C code analysis.

A two-day workshop at La Ferté Saint-Aubin for the LMV team.