Publications

Given an input program, sound static analyzers compute a list of potential runtime errors in it. Static analysis practitioners have difficulties measuring the precision of static analyzers and comparing their results. In this work, we formalize a notion of transparent static analyzers providing a fine-grained output of the proof obligations they verified. This transparent output enables a semantics-directed, fine-grained comparison and the combination of static analyzers. We introduce the Open Verification Dashboard (OVD), which provides a unified interface to aggregate the results of multiple static analyzers. By juxtaposing verified properties and outstanding warnings, OVD highlights coverage gaps, variabilities and inconsistencies across tools. We experimentally evaluate the benefits of OVD on benchmarks from the Competition on Software Verification (SV-COMP). This work paves the way for a static analysis standard for C runtime error reporting.

Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by isolated components. This works well as long as components do not share or expose their internal state: Any state update that is locally sound is also globally sound. However, some abstract domains require shared state, most prominently relational abstract domains, which use symbolic expressions such as 2x+5 to represent abstract values. As the relational component performs a strong update of x, the abstract value 2x+5 can change non-monotonically, which breaks soundness. We propose a novel solution to this problem: A virtual recency abstractions that decouples the relational component, supports strong updates, and allows recursion. We prove that the virtual recency abstraction restores soundness: Any shared state wrapped in our virtual recency abstraction may be locally updated non-monotonically, while global soundness persists. We applied our approach to develop the first relational WebAssembly analysis, reusing many components from an existing inter-procedural abstract interpreter. Furthermore, we evaluate the recall, precision, and scalability of this analysis to demonstrate the practicality of the virtual recency abstraction.

Data containers, such as lists, arrays, trees, etc, raise challenges for program verification. In static analysis by abstract interpretation, one popular approach is summarization: multiple elements of a data structure are abstracted into a single one, favoring performance over precision. This technique is at the core of most container abstractions – from smashing to segmentation – of arrays, lists or algebraic data types. However, summarization approaches are unable to express relations between containers, even when relational numerical abstract domains are used. Our work introduces DelExp, a new domain able to express relations between summarized variables. DelExp can state that the content of a data structure is included in the content of another data structure, up to a given transformation. DelExp is language-agnostic, modular in the abstraction chosen for any other types (integers, strings, functions, etc.), and can be seamlessly combined with existing container abstractions. We show how DelExp allows us to infer precise summaries for compositional analyses of container-manipulating functions in a pure functional language. We present extensions to DelExp supporting polymorphism and higher-order transformations. Our implementation of DelExp within the MOPSA static analysis platform confirms that DelExp works out of the box with pre-existing container abstractions. Our evaluation targets both Python programs manipulating lists and relational summary generation for OCaml functions handling algebraic data types.

We present advances we brought to Mopsa for SV-COMP 2026. Mopsa now supports a backward analysis mode which computes an under-approximation of the weakest liberal precondition for the alarms found during a verification pass, which generates an input harness to reproduce the incorrectness condition. We also added support for termination checking through the introduction of loop counters. With these improvements, Mopsa wins the SoftwareSystems category, and ranks third in the TrueOverall category.

FAIR principles are a set of guidelines aiming at simplifying the distribution of scientific data to enhance reuse and reproducibility. This article focuses on research software, which significantly differs from data in its living nature, and its relationship with free and open-source software. We provide a tiered roadmap to improve the state of research software, which takes into account the full range of stakeholders in the research software ecosystem: all scientific staff – regardless of prior software engineering training – but also institutions, funders, libraries and publishers.

Public administrations are steadily digitalizing all their procedures. In particular, computational laws – such as taxes and benefits – are increasingly implemented within computers, enabling scalable, automated computations. These computer implementations have four key specificities: they are critical software at the intersection between law and computer science, that will be updated regularly by legal changes, and have a long lifespan, counted in decades. Thus, great care should be taken to avoid any issue in these specific legal implementations. Building upon years of studying and coding computational laws, both in administrations and as new research products, we propose 20 recommendations to ease the development and maintenance of legal implementations. These recommendations aim at being understandable for lawyers and computer scientists alike.

Static analyzers are complex pieces of software with large dependencies. They can be difficult to install, which hinders adoption and creates barriers for students learning static analysis. This work introduces Try-Mopsa: a scaled-down version of the Mopsa static analysis platform, compiled into JavaScript to run purely as a client-side application in web browsers. Try-Mopsa provides a responsive interface that works on both desktop and mobile devices. Try-Mopsa features all the core components of Mopsa. In particular, it supports relational numerical domains. We present the interface, changes and adaptations required to have a pure JavaScript version of Mopsa. We envision Try-Mopsa as a convenient platform for onboarding or teaching purposes.

From short scripts to vast simulations of Earth’s climate, protein structures or even the cosmos, it is hard to imagine scientific research without software. Scientists use software code in myriad ways -to plan experiments; to record, organize, analyse, visualize and archive data; to control scientific instruments, and more. But software evolves. Most open-source software used in research is refined both iteratively and collectively, and has no published ‘version of record’. Updates can target various versions and releases, meaning that each aspect of the software -the project as a whole, a specific version or a single file -can require a different way to refer to it. This creates confusion. And so software comes with a double bind: like data, it supports the findings of a study and should be preserved and published. Yet it should also remain available and supported, and possibly be improved, over time. Scholars, librarians, research institutions and funding agencies are wrestling with how to reconcile these two requirements.

Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their recursive functions, recursive algebraic data types, and higher-order functions. Classic type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants. Our work describes a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. The summaries can be viewed as input-output relations expressed with relational abstract domains. We present two new abstract domains. A first abstract domain summarizes recursive algebraic data types. A second abstract domain lifts existing disjunctive relational summaries to higher-order by formalizing them as domains able to abstract higher-order functions. Both abstractions are parameterized by the abstractions of basic types (strings, integers, . . . ). Thanks to this parametric nature, both domains can be combined, allowing the analysis of higher-order functions manipulating algebraic data types and, conversely, algebraic data types using functions as first-class values. We have implemented this analysis in the open-source MOPSA platform. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs as well as 20 programs from the state-of-the-art Salto analyzer benchmark.

We present advances we brought to Mopsa for SV-Comp 2025. Most notably, Mopsa now supports bounded trace partitioning, constant widening with thresholds, and can check that all memory has been correctly deallocated. Further, Mopsa now integrates a sound support of bitfields. While Mopsa at SV-Comp previously relied on a fixed, homogeneous set of configurations to verify tasks, it can now automatically leverage semantic information from a previous analysis to trigger heuristic precision improvements in further analyses. With these improvements, Mopsa wins a silver medal in the SoftwareSystems category and ranks fifth in the NoOverflows category.

Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs intended to faithfully transcribe the law into computer code. Bugs in these programs can lead to dramatic societal impact, e.g., paying employees incorrect amounts, or not awarding benefits to families in need. To address this issue, we consider concolic unit testing, a combination of concrete execution with SMT-based symbolic execution, and propose CUTECat, a concolic execution tool targeting implementations of computational laws. Such laws typically follow a pattern where a base case is later refined by many exceptions in following law articles, a pattern that can be formally modeled using default logic. We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala, a recent domain-specific language tailored to implement computational laws. We evaluate CUTECat on several programs, including the Catala implementation of the French housing benefits and Section 132 of the US tax code. We show that CUTECat can successfully generate hundreds of thousands of testcases covering all branches of these bodies of law. Through several heuristics, we improve CUTECat’s scalability and usability, making the testcases understandable by lawyers and programmers alike. We believe CUTECat thus paves the way for the use of formal methods during legislative processes.

Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some need to be maintained in order to enable building further research upon the implementation. While necessary, these processes can be quickly challenging. This article documents the tools and techniques we have come up with to simplify the maintenance of Mopsa since 2017. Mopsa is a static analysis platform that aims at being sound. First, we describe an automated way to measure precision that does not require any baseline of true bugs obtained by manually inspecting the results. Further, it improves transparency of the analysis, and helps discovering regressions during continuous integration. Second, we have taken inspiration from standard tools observing the concrete execution of a program to design custom tools observing the abstract execution of the analyzed program itself, such as abstract debuggers and profilers. Finally, we report on some cases of automated testcase reduction.

Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users. In this work, we aim to provide a solid foundation for date arithmetic working on days, months and years. We first present a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F⋆ proof assistant. Building upon this semantics, we then propose a static analysis by abstract interpretation to automatically detect ambiguities in date computations. We finally integrate our approach in the Catala language, a recent domain-specific language for formalizing computational law, and use it to analyze the Catala implementation of the French housing benefits, leading to the discovery of several date-related ambiguities.

We present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of dynamic memory allocation, library calls such as memset, goto-based loops, and integer abstractions. We introduced a witness validator for correctness witnesses. Thanks to these improvements, Mopsa won SV-Comp’s SoftwareSystems category by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.

Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in order to offer extensibility and cooperation between them, which is especially beneficial when relational numerical domains are used. The analyses are currently flow-sensitive and fully context-sensitive. We focus only on proving programs to be correct, as our analyses are designed to be sound and terminating but not complete. We present our first participation to SV-Comp, where Mopsa earned a bronze medal in the SoftwareSystems category.

Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages ; cependant, aucun analyseur mature ne cible l’analyse de valeurs pour un langage fonctionnel à la ML. Des outils de vérification pour ces langages existent, tels les systèmes de types classiques ou les méthodes déductives, mais le raisonnement automatique sur des programmes numériques a jusqu’alors été peu exploré. Cet article décrit un analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel typé du premier ordre, approche sûre et automatique pour garantir l’absence d’erreurs à l’exécution. En se basant sur des domaines abstraits relationnels et en réalisant des résumés des champs récursifs des types algébriques, cette approche permet d’analyser des fonctions récursives manipulant des types algébriques récursifs et d’inférer dans un domaine abstrait leur relation entrée-sortie. Une implémentation est en cours sur la plateforme d’analyse multilangage MOPSA et analyse avec succès de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs précise et relationnelle basée sur l’interprétation abstraite pour les langages fonctionnels d’ordre supérieur à la ML.

Modern programs are increasingly multilanguage, to benefit from each programming language’s advantages and to reuse libraries. For example, developers may want to combine high-level Python code with low-level, performance-oriented C code. In fact one in five of the 200 most-downloaded Python libraries available on GitHub contain C code. Static analyzers tend to focus on a single language, and may use stubs to model the behavior of foreign function calls. However, stubs are costly to implement and undermine the soundness of analyzers. In this work we design a static analyzer by abstract interpretation that can handle Python programs calling C extensions. It analyses directly and fully automatically both the Python and the C source codes. It reports runtime errors that may happen in Python, in C, and at the interface. We implemented our analysis in a modular fashion: it reuses off-the-shelf C and Python analyses written in the same analyzer. This approach allows sharing between abstract domains of different languages. Our analyzer can tackle tests of real-world libraries a few thousand lines of C and Python long.

Mopsa est un logiciel de vérification de programmes par analyse statique sûre basée sur la théorie de l’interprétation abstraite. Il infère automatiquement des invariants et détecte, à la compilation, les erreurs possibles à l’exécution. L’analyse calcule une interprétation des programmes dans une collection d’abstractions réutilisables et programmées en OCaml. Sa conception modulaire permet à Mopsa d’être extensible vis à vis des propriétés et des langages considérés. Mopsa supporte actuellement des sous-ensembles significatifs des langages C et Python 3. En C, Mopsa détecte les comportements indéfinis ainsi que l’utilisation invalide de la bibliothèque standard C (spécifiée dans un langage de modélisation dédié). En Python, Mopsa effectue une analyse de type, de valeur et des exceptions. La démonstration présentera l’utilisation de Mopsa à travers quelques exemples simples en C et en Python. Elle mettra en évidence l’intérêt d’une conception modulaire en montrant comment, d’une part, un changement des abstractions utilisées permet d’éliminer des faux positifs et, d’autre part, comment une même abstraction est exploitée dans l’analyse de langages aussi différents que C et Python.

Once per year, the French Directorate for Public Finances (DGFiP) computes for each citizen the amount of income tax owed to the State, depending on their earnings reported on their tax return. This computation is largely automated and performed by a computer program. The source code is written partly in a custom domain specific language called M (used only by the DGFiP), and published yearly. The other part is written in C, and has never been released. Thanks to a mix of retro-engineering and code refactoring, we are able to present Mlang: an open-source toolchain allowing to reproduce the French income tax computation.

In France, income tax is computed from taxpayers’ individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP). This algorithm relies on a legacy custom language and compiler originally designed in 1990, which unlike French wine, did not age well with time. Owing to the shortcomings of the input language and the technical limitations of the compiler, the algorithm is proving harder and harder to maintain, relying on ad-hoc behaviors and workarounds to implement the most recent changes in tax law. Competence loss and aging code also mean that the system does not benefit from any modern compiler techniques that would increase confidence in the implementation. We overhaul this infrastructure and present Mlang, an open-source compiler toolchain whose goal is to replace the existing infrastructure. Mlang is based on a reverse-engineered formalization of the DGFiP’s system, and has been thoroughly validated against the private DGFiP test suite. As such, Mlang has a formal semantics; eliminates previous hand-written workarounds in C; compiles to modern languages (Python); and enables a variety of instrumentations, providing deep insights about the essence of French income tax computation. The DGFiP is now officially transitioning to Mlang for their production system.

Python is an increasingly popular dynamic programming language, particularly used in the scientific community and well-known for its powerful and permissive high-level syntax. Our work aims at detecting statically and automatically type errors. As these type errors are exceptions that can be caught later on, we precisely track all exceptions (raised or caught). We designed a static analysis by abstract interpretation able to infer the possible types of variables, taking into account the full control-flow. It handles both typing paradigms used in Python, nominal and structural, supports Python’s object model, introspection operators allowing dynamic type testing, dynamic attribute addition, as well as exception handling. We present a flow- and context-sensitive analysis with special domains to support containers (such as lists) and infer type equalities (allowing it to express parametric polymorphism). The analysis is soundly derived by abstract interpretation from a concrete semantics of Python developed by Fromherz et al. Our analysis is designed in a modular way as a set of domains abstracting a concrete collecting semantics. It has been implemented into the MOPSA analysis framework, and leverages external type annotations from the Typeshed project to support the vast standard library. We show that it scales to benchmarks a few thousand lines long, and preliminary results show it is able to analyze a small real-life command-line utility called PathPicker. Compared to previous work, it is sound, while it keeps similar efficiency and precision.

Sound static analyses for large subsets of static programming languages such as C are now widespread. For example the Astrée static analyzer soundly overapproximates the behavior of C programs that do not contain any dynamic code loading, longjmp statements nor recursive functions. The sound and precise analysis of widely used dynamic programming languages like JavaScript and Python remains a challenge. This paper examines the variation of static analyses of Python – in precision, time and memory usage – by adapting three parameters: (i) the value sensitivity, (ii) the allocation sensitivity and (iii) the activation of an abstract garbage collector. It is not clear yet which level of sensitivity constitutes a sweet spot in terms of precision versus efficiency to achieve a meaningful Python analysis. We thus perform an experimental evaluation using a prototype static analyzer on benchmarks a few thousand lines long. Key findings are: the value analysis does not improve the precision over type-related alarms; the value analysis is three times costlier than the type analysis; the allocation sensitivity depends on the value sensitivity; using an abstract garbage collector lowers memory usage and running times, but does not affect precision.

Le code des impôts définit dans son texte législatif une fonction mathématique permettant de calculer l’impôt sur le revenu d’un foyer fiscal. Afin de recouvrer l’impôt, cette fonction est implémentée sous la forme d’un algorithme par la Direction Générale des Finances Publiques (DGFiP), en utilisant un langage dédié appelé M (pour macro-langage). Nous proposons une sémantique formelle du langage M, testée grâce aux données publiées par la DGFiP. Cette formalisation, couplée à la publication par la DGFiP de la base de code M calculant l’impôt, nous donne accès à une formalisation complète de la portion du code des impôts définissant l’algorithme de calcul de l’impôt sur le revenu. Nous démontrons l’utilité d’une telle formalisation grâce à un prototype à base de solveurs SMT permettant d’inférer des méta-propriétés sur le calcul de l’impôt. Ces méta-propriétés peuvent ensuite compléter et affiner les analyses économiques existantes sur les effets redistributifs de l’impôt sur le revenu, mais aussi de diverses allocations. Plus généralement, une formalisation systématique des portions algorithmiques de la loi permettrait d’augmenter le niveau d’assurance sur la cohérence du système socio-fiscal français.
Trois artefacts logiciels accompagnent cet article : une formalisation mécanisée de la sémantique du langage M, un compilateur pour le langage M basé sur cette sémantique, ainsi que le prototype d’encodage du code des impôts dans le solveur SMT Z3.

See also: Gallium’s talk with Denis

We discuss the design of Mopsa, an ongoing effort to design a novel semantic static analyzer by abstract interpretation. Mopsa strives to achieve a high degree of modularity and extensibility by considering value abstractions for numeric, pointer, objects, arrays, etc. as well as syntax-driven iterators and control-flow abstractions uniformly as domain modules, which offer a unified signature and loose coupling, so that they can be combined and reused at will. Moreover, domains can dynamically rewrite expressions, which simplifies the design of relational abstractions, encourages a design based on layered semantics, and enables domain reuse across different analyses and different languages. We present preliminary applications of Mopsa analyzing simple programs in subsets of the C and Python programming languages, checking them for run-time errors and uncaught exceptions.

Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepancy between continuous reals and discrete finite-precision values, automated static analysis tools are highly valuable to estimate roundoff errors. The results, however, are only as correct as the implementations of the static analysis tools. This paper presents a formally verified and modular tool which fully automatically checks the correctness of finite-precision roundoff error bounds encoded in a certificate. We present implementations of certificate generation and checking for both Coq and HOL4 and evaluate it on a number of examples from the literature. The experiments use both in-logic evaluation of Coq and HOL4, and execution of extracted code outside of the logics: we benchmark Coq extracted unverified OCaml code and a CakeML-generated verified binary.

We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments and comparison with ConcurInterproc show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.