Author: lmvadm

[July 2025] Talk by Loïc Correnson

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.

[July 2025] Talk by Virginia Niculescu

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.

[July 2025] Talk by André Maroneze

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.

[June 2025] Talk by Davide Catta

First Order Coalition Logic : Model Checking, Complétude et Satisfaisabilité
Davide Catta (LIPN, Paris 13)
June 25, 2025
Les logiques pour le raisonnement stratégique constituent une vaste famille d’outils formels conçus pour modéliser, vérifier et analyser les capacités et les stratégies (individuels ou collectifs) d’agents autonomes, dans un environnement compétitif.
Nous introduisons First Order Coalition Logic (FOCL), qui combine les intuitions de Coalition Logic (CL) et de Strategy Logic (SL). Plus précisément, FOCL permet une quantification arbitraire sur les actions de groupes d’agents.
Dans cet exposé, nous montrons que FOCL est strictement plus expressive que d’autres logiques de coalition connues, puis nous discutons de sa procédure de model checking. Ensuite, nous fournissons une axiomatisation cohérente et complète de cette logique, qui est, à notre connaissance, la première axiomatisation d’une logique stratégique dans la littérature. Enfin, nous montrons que le problème de la satisfaisabilité est indécidable.

[June 2025] Five members of the LMV Team at the Journées Nationales du GdR GPL & Journées AFADL

These national conference are in Pau from June 16 to June 19. Myriam Clouet presents her work Monday at 2PM, Jordan Ischard presents his work on Tuesday at 11:50AM, Frédéric Loulergue gives a keynote Wednesday at 9AM, Terence Clastres presents his poster and Frédéric Dabrowski chairs the CLAP session on Thursday afternoon.