2025Activity reportProject-TeamTOCCATA
RNSR: 201221053L- Research center Inria Saclay Centre at Université Paris-Saclay
- In partnership with:CNRS, Université Paris-Saclay
- Team name: Certified Programs, Certified Tools, Certified Floating-Point Computations
- In collaboration with:Laboratoire de Méthodes Formelles
Creation of the Project-Team: 2014 July 01
Each year, Inria research teams publish an Activity Report presenting their work and results over the reporting period. These reports follow a common structure, with some optional sections depending on the specific team. They typically begin by outlining the overall objectives and research programme, including the main research themes, goals, and methodological approaches. They also describe the application domains targeted by the team, highlighting the scientific or societal contexts in which their work is situated.
The reports then present the highlights of the year, covering major scientific achievements, software developments, or teaching contributions. When relevant, they include sections on software, platforms, and open data, detailing the tools developed and how they are shared. A substantial part is dedicated to new results, where scientific contributions are described in detail, often with subsections specifying participants and associated keywords.
Finally, the Activity Report addresses funding, contracts, partnerships, and collaborations at various levels, from industrial agreements to international cooperations. It also covers dissemination and teaching activities, such as participation in scientific events, outreach, and supervision. The document concludes with a presentation of scientific production, including major publications and those produced during the year.
Keywords
Computer Science and Digital Science
- A2.1.1. Semantics of programming languages
- A2.1.4. Functional programming
- A2.1.6. Concurrent programming
- A2.1.10. Domain-specific languages
- A2.1.11. Proof languages
- A4.5.2. Model-checking
- A4.5.3. Program proof
- A6.2.1. Numerical analysis of PDE and ODE
- A7.2. Logic in Computer Science
- A7.2.1. Decision procedures
- A7.2.2. Automated Theorem Proving
- A7.2.3. Interactive Theorem Proving
- A7.2.4. Mechanized Formalization of Mathematics
- A8.10. Computer arithmetic
Other Research Topics and Application Domains
- B5.2.2. Railway
- B5.2.3. Aviation
- B5.2.4. Aerospace
- B6.1. Software industry
- B9.5.1. Computer science
- B9.5.2. Mathematics
1 Team members, visitors, external collaborators
Research Scientists
- Claude Marché [Team leader, INRIA, Senior Researcher, HDR]
- Sylvie Boldo [INRIA, Senior Researcher, HDR]
- Jean-Christophe Filliâtre [CNRS, Senior Researcher, HDR]
- Armaël Guéneau [INRIA, Researcher, until Aug 2025]
- Guillaume Melquiond [INRIA, Senior Researcher, until Sep 2025, HDR]
Faculty Members
- Sylvain Conchon [Université Paris-Saclay, Professor, HDR]
- Florent Hivert [Université Paris-Saclay, Professor, until Aug 2025, Délégation Inria, HDR]
- Micaela Mayero [Université Sorbonne Paris-Nord, Professor, until Sep 2025, Délégation Inria, HDR]
- Andrei Paskevich [Université Paris-Saclay, Associate Professor]
Post-Doctoral Fellow
- Oregane Desrentes [INRIA, Post-Doctoral Fellow, from Oct 2025]
PhD Students
- Paul Geneau De Lamarlière [Mitsubishi Electric R&D Centre Europe, CIFRE]
- Arnaud Golfouse [INRIA]
- David Hamelin [EDF, CIFRE]
- Vincent Lafeychine [Université Paris-Saclay, from Sep 2025]
- Josué Moreau [INRIA]
- Paul Patault [Université Paris-Saclay]
- Henri Saudubray [Université Paris-Saclay, from Oct 2025]
Technical Staff
- Noé Canva [INRIA, Engineer, from Apr 2025]
- Maëll Coulmance [INRIA, Engineer, from Nov 2025]
- Matteo Manighetti [INRIA, Engineer, until Mar 2025]
- Li-Yao Xia [INRIA, Engineer]
Interns and Apprentices
- Oualid Chabane [INRIA, Intern, from May 2025 until Jul 2025]
- Vincent Lafeychine [LMF, Intern, from Mar 2025 until Aug 2025]
- Ilian Woerly [INRIA, Intern, from May 2025 until Jul 2025]
Administrative Assistant
- Joyce Soares Brito [INRIA]
External Collaborators
- Thibaut Balabonski [LMF]
- Jacques-Henri Jourdan [LMF]
- Chantal Keller [LMF]
2 Overall objectives
The general objective of the Toccata project is to promote formal specification and computer-assisted proof in the development of software that requires high assurance in terms of safety and correctness with respect to its intended behaviour. Such safety-critical software appears in many application domains like transportation (e.g. aviation, aerospace, railway, automotive), communication (e.g. internet, smartphones), health devices, data management on clouds (confidentiality issues), etc. The number of tasks performed by software is quickly increasing, together with the number of lines of code involved. Given the need of high assurance of safety in the functional behaviour of such applications, the need for automated (in the sense computer-assisted) methods and techniques to bring guarantee of safety became a major challenge. In the past and at present, the most widely used approach to check safety of software is to apply heavy test campaigns, which take a large part of the costs of software development. Yet these campaigns cannot ensure that all the bugs are caught, and remaining bugs may have catastrophic consequences.
Generally speaking, software verification approaches pursue three goals: (1) verification should be sound, in the sense that no bugs should be missed, (2) verification should not produce false alarms, or as few as possible, (3) it should be as automatic as possible. Reaching all three goals at the same time is a challenge. A large class of approaches emphasises goals (2) and (3): testing, run-time verification, symbolic execution, model checking, etc. Static analysis, such as abstract interpretation, emphasises goals (1) and (3). Deductive verification emphasises (1) and (2). The Toccata project is mainly interested in exploring the deductive verification approach, although we also combine with the other techniques occasionally.
In the past decade, significant progress has been made in the domain of deductive program verification. This is emphasised by some success stories of application of these techniques on industrial-scale software. For example, the Atelier B system was used to develop part of the embedded software of the Paris metro line 14 43 and other railway-related systems; a formally proved C compiler was developed using the Coq proof assistant 73; the L4-verified project developed a formally verified micro-kernel with high security guarantees, using analysis tools on top of the Isabelle/HOL proof assistant 72. A bug in the JDK implementation of TimSort was discovered using the KeY environment 69 and a fixed version was proved sound. Another sign of recent progress is the emergence of deductive verification competitions (e.g. VerifyThis 45). Finally, recent trends in the industrial practice for development of critical software is to require more and more guarantees of safety, e.g. the DO-178C standard for developing avionics software adds to the former DO-178B the use of formal models and formal methods. It also emphasises the need for certification of the analysis tools involved in the process.
3 Research program
Panorama of Deductive Verification
There are two main families of approaches for deductive verification. Methods in the first family build on top of mathematical proof assistants (e.g. Coq, Isabelle) in which both the model and the program are encoded; the proof that the program meets its specification is typically conducted in an interactive way using the underlying proof construction engine. Methods from the second family proceed by the design of standalone tools taking as input a program in a particular programming language (e.g. C, Java) specified with a dedicated annotation language (e.g. ACSL 44, JML 56) and automatically producing a set of mathematical formulas (the verification conditions) which are typically proved using automatic provers (e.g. Z3 78, Alt-Ergo 58, CVC5 42).
The first family of approaches usually offers a smaller Trusted Code Base (TCB) than the second, but also demands more work to perform the proofs (because of their interactive nature) and makes them less easy to adopt by industry. Moreover, they generally do not allow to directly analyse a program written in a mainstream programming language like Java or C. The second kind of approaches has benefited in the past years from the tremendous progress made in SAT and SMT solving techniques, allowing more impact on industrial practices, but suffers from a lower level of trust: in all parts of the proof chain (the model of the input programming language, the VC generator, the back-end automatic prover), potential errors may appear, compromising the guarantee offered. Moreover, while these approaches are applied to mainstream languages, they usually support only a subset of their features.
Overall Goals of the Toccata Project
One of our original skills is the ability to conduct proofs by using automatic provers and proof assistants at the same time, depending on the difficulty of the program, and specifically the difficulty of each particular verification condition. We thus believe that we are in a good position to propose a bridge between the two families of approaches of deductive verification presented above. Establishing this bridge is one of the goals of the Toccata project: we want to provide methods and tools for deductive program verification that can offer both a high amount of proof automation and a high guarantee of validity.
In industrial applications, numerical calculations are very common (e.g. control software in transportation). Typically they involve floating-point numbers. Some of the members of Toccata have an internationally recognised expertise on deductive program verification involving floating-point computations. Our past work includes a new approach for proving behavioural properties of numerical C programs using Frama-C/Jessie 38, various examples of applications of that approach 49, the use of the Gappa solver for proving numerical algorithms 64, an approach to take architectures and compilers into account when dealing with floating-point programs 51, 80. We also contributed to the Handbook of Floating-Point Arithmetic 79 and co-published a survey on floating-point arithmetic 4. A representative case study is the analysis and the proof of both the method error and the rounding error of a numerical analysis program solving the one-dimension acoustic wave equation 4746. Our experience led us to a conclusion that verification of numerical programs can benefit a lot from combining automatic and interactive theorem proving 48, 49, 67, 68. Verification of numerical programs is another main axis of Toccata.
Let us conclude with more general considerations: we want to keep on with general audience actions and industrial transfer through sustained long-term collaboration with industrial partners (Section 4). Our scientific programme detailed below is structured into the following four axes.
- Foundations and spreading of deductive program verification;
- Reasoning on mutable memory in program verification;
- Verification of Computer Arithmetic;
- Spreading Formal Proofs.
3.1 Foundations and spreading of deductive program verification
This axis covers the fundational studies we pursue regarding deductive verification. A non-exhaustive list of subjects we want to address is as follows.
- The search for improved methods to generate verification conditions, relying for example on new calculi, on better notion of abstraction, or on automatic discovery of invariants.
- Uniform approaches to obtain correct-by-construction programs and libraries, in particular by automatic extraction of executable code (in OCaml, C, CakeML, etc.) from verified programs, and including innovative general methods like advanced ghost code, ghost monitoring, etc. A representative publication is the presentation of a new notion called ghost monitors 57.
- Improvement of automated reasoning techniques: methods dedicated to deductive verification, so as to improve proof automation; improved combination of interactive provers and fully automated ones, proof by reflection.
- Providing feedback in case of proof failures, e.g. based on generation of counterexamples, or symbolic execution.
The Why3 ecosystem in 2025
A significant part of the work achieved in this axis is related to the Why3 toolbox and its ecosystem, displayed on Figure 1. The red background boxes represent tools that we develop ourselves, whereas blue background ones are developed by others. SPARK2014 is developed by AdaCore. Frama-C and Wp are developed by CEA-list and directly produce logical formulas to be passed to provers. TIS-Analyzer is developed by TrustInSoft and J is a collaboration between TrustInSoft and us. We develop the front-ends micro-C and micro-Python mainly for teaching purpose. The front-end for Ladder programs is a software developed internally by MERCE. The front-end Cameleer 81 is developed at Nova School of Science and Technology, Lisbon, Portugal. Yellow background boxes represent libraries of specifications of logic data-types with their logical properties. A representative publication is an article on abstraction and genericity features of Why3 7.
3.2 Reasoning on mutable memory in program verification
This axis concerns specifically the techniques for reasoning on programs where memory aliasing is the central issue. It covers the methods based on type-based alias analysis and related memory models, on specific program logics such as separation logics, and extended model-checking. It concerns the application on analysis of C or C++ codes, on Ada codes involving pointers, but also concurrent programs in general. The main topics are:
- The study of advanced type systems dedicated to verification, for controlling aliasing, and their use for obtaining easier-to-prove verification conditions. Modern typing systems in the style of Rust, involving ownership and borrowing, are considered. A representation publication is a paper 9 on the semantic foundation of the verification of Rust programs.
- The design of front-ends of Why3 for the proofs of programs where aliasing cannot be fully controlled statically, via adequate memory models, aiming in particular at extraction to C; and also for concurrent programs.
- The continuation of fruitful work on concurrent parameterised systems, and its corresponding specific SMT-based model-checking. Reference publication are 5 and 6.
There are also other various topics considered in this axis, for example around capability machines, which denote a type of CPU allowing fine-grained privilege separation using capabilities, with machine words that represent certain kinds of authority. Guéneau et al. 8 present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. Other topics concern reasoning on resources 82, and cross-language verification 70.
3.3 Verification of Computer Arithmetic
This axis, which bridges the domains of computer arithmetic and of formal verification, is a major originality of Toccata. The main topics are as follows.
- We are studying the fundamental blocks of formalising floating-point computations, algorithms, and error analysis.
- A significant effort is dedicated to verification of numerical programs written in mainstream languages such as C or Ada. This involves combining specifications in real numbers and computation in floating-point, and underlying automated reasoning techniques with floating-point numbers and real numbers. We also contributed to the automation of reasoning on floating-point numbers 60.
- Related to the formalisation of mathematics, we aim at verifying numerical analysis programs, in particular numerical schemes for solving partial differential equations. A representative publication is a paper on the formalisation of Lebesgue integration 3 and a paper on certified approximations of integrals 74.
Boldo and Melquiond are authors of a reference book 50 on the formal verification of numerical programs.
3.4 Spreading Formal Proofs
The general goal of this axis, which was a new one proposed in 2019, was to encourage spreading of deductive verification through actions showing how our methods and tools can be used on programs that we develop ourselves. Since this axis is dedicated to applications in a general manner, positioning barely makes sense since a vast majority of research groups in computer science in the world would claim to conduct case studies and large-scale applications.
Representative of these significant case studies are the automated analysis of Debian packages installation 1, a certified library for arbitrary-precision arithmetic 10, and the automated analysis of Ladder programs 2.
4 Application domains
4.1 Industrial Transfer Actions
The application domains we target involve safety-critical software, that is where a high-level guarantee of soundness of functional execution of the software is wanted. Currently our industrial collaborations or impact mainly belong to the domain of transportation: aerospace, aviation, railway, automotive.
-
Transfer to the community of Atelier B
in the context of the FUI project LCHIP, we investigated the use of Why3 and Alt-Ergo as an alternative back-end for checking proof obligations generated by Atelier B, whose main applications are railroad-related.
-
ProofInUse-AdaCore collaboration: transfer to the community of
Ada development
Since the creation of the ProofInUse joint lab in 2014, with AdaCore company, we have a growing impact on the community of industrial development of safety-critical applications written in Ada. See that web page for a an overview of AdaCore's customer projects, in particular those involving the use of the SPARK Pro tool set. This impact involves both the use of Why3 for generating VCs on Ada source codes, and the use of Alt-Ergo for performing proofs of those VCs. This action allowed AdaCore company to get new customers, in particular the domains of application of deductive formal verification are from the historical domain of aerospace (e.g. this link or this link) but went beyond: application in automotive (e.g. Denso, Toyata), medical and security (e.g. Nvidia). A joint publication of Nvidia and AdaCore 37 in 2023 exposes, with their own words, the benefit of using high level verification for securing Nvidia chips.
-
ProofInUse-TrustInSoft collaboration
In 2017 we started to collaborate with the TrustInSoft company for the verification of C and C++ codes. We started with a CIFRE thesis funding, which explored the use of Why3 to design verified and reusable C libraries 83, and then with a bilateral contract towards the design of the J plugin in TIS-Analyzer, bringing deductive verification techniques in this platform, including counterexamples when proofs fail. The impact on TrustInSoft customers is not yet easily identifiable; it will hopefully increase in particular in the context of the project Décysif led by TrustInSoft, from 2022 to 2027.
-
ProofInUse-MERCE collaboration
In 2019 we started to collaborate with Mitsubishi Electric R&D Centre Europe in Rennes, France. The R&D programme is two-fold: first the verification of Ladder programs for PLCs, second the verification of numerical C codes. MERCE has now a mature platform for Ladder verification, which has yet to be made really usable by development teams. This work received the FMICS best paper award in 2021. The work of numerical programs is increasing in importance. We have results on log-sum-exp functions 53, 54 and a CIFRE thesis started in 2023, aiming at designing better proof environments for verifying programs with complex numeric computations. A patent entitled Automatic implementation of formally-verified numerical programs has been filled in 2022 at EPO. A new axis of collaboration with MERCE started in 2024, regarding the validation of invariants on data representing railway networks 33.
-
CIFRE thesis with EDF
We are starting at the end of 2024 a collaboration with EDF by the CIFRE thesis of David Hamelin about computer arithmetic aspects of EDF qualified codes.
Generally speaking, we believe that our increasing industrial impact is a representative success for our general goal of spreading deductive verification methods to a larger audience, and we are firmly engaged into continuing such kind of actions in the next years.
4.2 Other socio-economic impact
We believe our impact is not limited to industrial actions per se.
A first point is that during the years, the young students that we train, either as a PhD position or a temporary engineer positions, easily got positions in private companies. Indeed we believe we can say that we contributed to the creation of jobs in several companies.
Another important part of our social impact is our work with high school students. With new curricula including more computer science than ever before, it was important to provide good reference books. With this in mind, we have contributed three books aimed at high school and preparatory school students 40, 39, 41.
The impact is not limited to books: we also helped a teacher to design a lesson to learn the basic notions of program verification (say: loop invariants) using the Why3 tool (article IREMI). We are also part each year of stands at “Fête de la science” in November or special events towards girls. We also often go to (high) schools for presenting either our job or our research (except during the COVID pandemic).
The social impact in national education is finally made highly evident by our implication in the organisation of the agrégation d'informatique which is in charge to select and recruit the best high-level teachers for the new programmes.
5 Social and environmental responsibility
5.1 Footprint of research activities
Our research activities make use of standard computers for developing software and developing formal proofs. We have no use of specific large size computing resources. Though, we are making use of external services for continuous integration. A continuous integration methodology for mature software like Why3 is indeed mandatory for ensuring a safe software engineering process for maintenance and evolution. We make the necessary efforts to keep the energy consumption of such a continuous integration process as low as possible.
Ensuring the reproducibility of proofs in formal verification is essential. It is thus mandatory to replay such proofs regularly to make sure that our changes in our software do not loose existing proofs. For example, we need to make sure that the case studies in formal verification that we present in our gallery are reproducible. We also make the necessary efforts to keep the energy consumption for replaying proofs low, by doing it only when necessary.
As widely accepted nowadays, the major sources of environmental impact of research is travel to international conferences by plane, and renewal of electronic devices. The number of travels we made in 2022 remained very low with respect to previous years, of course because of the Covid pandemic, and the fact that many conferences were now proposed online participation. We intend to continue limiting the environmental impact of our travels. Concerning renewal of electronic devices, that is mainly laptops and monitors, we have always been careful on keeping them usable for as long time as possible.
5.2 Impact of research results
Our research results aims at improving the quality of software, in particular in mission-critical contexts. As such, making software safer is likely to reduce the necessity for maintenance operations and thus reducing energy costs.
Our efforts are mostly towards ensuring the safety of functional behavior of software, but we also increasingly consider the verification of their time or memory consumption. Reducing those would naturally induce a reduction in energy consumption.
Our research never involve any processing of personal data, and consequently we have no concern about preserving individual privacy, and no concern with respect to the RGPD (Règlement Général sur la Protection des Données).
In 2024, S. Boldo was in the program committee of the first PROPL workshop (Programming for the Planet ) to see how we may help topics such as climate analysis, modelling, forecasting, policy, and diplomacy.
6 Highlights of the year
Learn Programming with OCaml 36 is a new book by Sylvain Conchon and Jean-Christophe Filliâtre. This is an English translation (by Urmila Nair) of the French edition “Apprendre à programmer avec OCaml” 59.
The book is available as a PDF file, under the CC-BY-SA license. The source code for the various programs contained in the book is available for download, under the same license.
The book is structured in two parts. The first part is a tutorial-like introduction to OCaml through 14 small programs, covering many aspects of the language. The second part focuses on fundamental algorithmic concepts, with data structures and algorithms implemented in OCaml.
7 Latest software developments, platforms, open data
7.1 Latest software developments
7.1.1 Alt-Ergo
-
Name:
Automated theorem prover for software verification
-
Keywords:
Software Verification, Automated theorem proving
-
Functional Description:
Alt-Ergo is an automatic solver of formulas based on SMT technology. It is especially designed to prove mathematical formulas generated by program verification tools, such as Frama-C for C programs, or SPARK for Ada code. Initially developed in Toccata research team, Alt-Ergo's distribution and support are provided by OCamlPro since September 2013.
- URL:
-
Contact:
Claude Marche
-
Participant:
5 anonymous participants
-
Partner:
OCamlPro
7.1.2 CoqInterval
-
Name:
Interval package for Coq
-
Keywords:
Interval arithmetic, Coq
-
Functional Description:
CoqInterval is a library for the proof assistant Coq.
It provides several tactics for proving theorems on enclosures of real-valued expressions. The proofs are performed by an interval kernel which relies on a computable formalization of floating-point arithmetic in Coq.
The Marelle team developed a formalization of rigorous polynomial approximation using Taylor models in Coq. In 2014, this library has been included in CoqInterval.
- URL:
-
Publications:
hal-04859533, hal-04702129, hal-04515714, hal-04114233, hal-03168208, tel-02194683, hal-01630143, hal-01289616, hal-00180138, hal-01086460, hal-00797913
-
Contact:
Guillaume Melquiond
-
Participant:
12 anonymous participants
7.1.3 Coquelicot
-
Name:
The Coquelicot library for real analysis in Coq
-
Keywords:
Coq, Real analysis
-
Functional Description:
Coquelicot is library aimed for supporting real analysis in the Coq proof assistant. It is designed with three principles in mind. The first is the user-friendliness, achieved by implementing methods of automation, but also by avoiding dependent types in order to ease the stating and readability of theorems. This latter part was achieved by defining total function for basic operators, such as limits or integrals. The second principle is the comprehensiveness of the library. By experimenting on several applications, we ensured that the available theorems are enough to cover most cases. We also wanted to be able to extend our library towards more generic settings, such as complex analysis or Euclidean spaces. The third principle is for the Coquelicot library to be a conservative extension of the Coq standard library, so that it can be easily combined with existing developments based on the standard library.
- URL:
- Publications:
-
Contact:
Guillaume Melquiond
-
Participant:
3 anonymous participants
7.1.4 Cubicle
-
Name:
The Cubicle model checker modulo theories
-
Keywords:
Model Checking, Software Verification
-
Functional Description:
Cubicle is an open source model checker for verifying safety properties of array-based systems, which corresponds to a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems.
- URL:
-
Contact:
Sylvain Conchon
-
Participant:
2 anonymous participants
7.1.5 Flocq
-
Name:
The Flocq formalization of floating-point arithmetic for the Coq proof assistant
-
Keyword:
Floating-point
-
Functional Description:
The Flocq library for the Coq proof assistant is a comprehensive formalization of floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. It provides a framework for developers to formally verify numerical applications.
Flocq is currently used by the CompCert verified compiler to support floating-point computations.
- URL:
- Publications:
-
Contact:
Guillaume Melquiond
-
Participant:
3 anonymous participants
7.1.6 Gappa
-
Name:
The Gappa tool for automated proofs of arithmetic properties
-
Keywords:
Floating-point, Arithmetic code, Software Verification, Constraint solving
-
Functional Description:
Gappa is a tool intended to help formally verifying numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to verify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.
- URL:
-
Publications:
hal-03233227, tel-02194683, inria-00070739, inria-00344518, inria-00070330, tel-01094485, inria-00071232, inria-00432726, ensl-00379167, ensl-00200830, hal-01110666, hal-01110669, hal-01632617
-
Contact:
Guillaume Melquiond
-
Participant:
2 anonymous participants
7.1.7 Why3
-
Name:
The Why3 environment for deductive verification
-
Keywords:
Formal methods, Trusted software, Software Verification, Deductive program verification
-
Functional Description:
Why3 is an environment for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
- URL:
-
Contact:
Claude Marche
-
Participant:
7 anonymous participants
-
Partners:
CNRS, Université Paris-Sud
7.1.8 Rocq
-
Name:
The Rocq Prover
-
Keyword:
Proof assistant
-
Scientific Description:
Rocq is an interactive proof assistant based on the Calculus of (Co-)Inductive Constructions, extended with universe polymorphism. This type theory features inductive and co-inductive families, an impredicative sort and a hierarchy of predicative universes, making it a very expressive logic. The calculus allows to formalize both general mathematics and computer programs, ranging from theories of finite structures to abstract algebra and categories to programming language metatheory and compiler verification. Rocq is organised as a (relatively small) kernel including efficient conversion tests on which are built a set of higher-level layers: a powerful proof engine and unification algorithm, various tactics/decision procedures, a transactional document model and, at the very top an integrated development environment (IDE).
-
Functional Description:
The Rocq Prover provides both a dependently-typed functional programming language and a logical formalism, which, altogether, support the formalisation of mathematical theories and the specification and certification of properties of programs. The Rocq Prover also provides a large and extensible set of automatic or semi-automatic proof methods. Rocq's programs are extractible to OCaml, Haskell, Scheme, ...
-
Release Contributions:
An overview of the new features and changes, along with the full list of contributors is available at https://rocq-prover.org/releases/9.1.0
-
News of the Year:
The Rocq Prover was renamed at the beginning of 2025 (see https://rocq-prover.org/about#Name for details on the name change).
Its current version is Rocq 9.1, which integrates changes to the Rocq kernel, performance improvements, and a few new features. See the detailed changes at https://rocq-prover.org/releases/9.1.0 for an overview, along with the full list of contributors.
- URL:
-
Contact:
Matthieu Sozeau
-
Participants:
Yves Bertot, Frédéric Besson, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Erik Martin Dorel, Guillaume Melquiond, Pierre-Marie Pedrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-Yao Xia, Theo Zimmermann
7.1.9 creusot
-
Name:
Creusot
-
Keywords:
Rust, Specification language, Deductive program verification
-
Functional Description:
Creusot is a tool for deductive verification of Rust code. It allows you to annotate your code with specifications, invariants and assertions and then verify them formally and automatically, proving, mathematically, that your code satisfies your specifications.
Creusot works by translating Rust code to WhyML, the verification and specification language of Why3. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions.
-
Release Contributions:
This is the version 0.8.0, providing the main process to go from a Rust program annotated with Pearlite specifications to a set of verifications conditions to be discharged by external SMT solvers.
- URL:
- Publications:
-
Contact:
Jacques-Henri Jourdan
-
Participant:
3 anonymous participants
-
Partners:
Université Paris-Saclay, CNRS
7.1.10 rocq-num-analysis
-
Name:
Numerical analysis Rocq library
-
Keywords:
Formal methods, Rocq, Numerical analysis, Finite element modelling
-
Scientific Description:
These Coq/Rocq developments are based on the Coquelicot library for real analysis, and on parts of the Mathematical Components library. They are based on classical logic. Version 2.1 includes the formalization and proof of: (1) results about subsets, functions, homogeneous binary relations, and finite families, (2) results in algebra about commutative monoids and groups, rings, vector and affine spaces, including functions to a given algrebraic structure, iterated operations (sum, linear combination, and barycenter), morphisms, algebraic substructures, and the specific case of finite dimension with the dimension and the incomplete basis theorems, (3) the Lax-Milgram theorem, including results from linear algebra, geometry, functional analysis and Hilbert spaces, (4) the Lebesgue integral, including large parts of the measure theory,the building of the Lebesgue measure on real numbers, integration of nonnegative measurable functions with the Beppo Levi (monotone convergence) theorem, Fatou's lemma, the Tonelli theorem, and the Bochner integral with the dominated convergence theorem, (5) simplicial Lagrange finite elements in any dimension and of any degre of approximation.
-
Functional Description:
Formal developments and proofs in Rocq of numerical analysis problems. The current long-term goal is to formally prove parts of a C++ library implementing the Finite Element Method.
-
News of the Year:
Several parts of the formalization in Coq/Rocq of simplicial Lagrange finite elements have been generalized, and the building of the FE is now almost exclusively based on affine properties involving barycenters. Opam packages (v2.0, 17/06/2025) are provided for each part of the library: subset, algebra, lebesgue, lax-milgram, and fem. A paper about the formalization of simplicial Lagrange finite elements is submitted. The version 2.1 of the Opam packages (24/11/2025) provides many modifications and new results about binary relations and orders. A paper about the formalization of monomial and graded orders is submitted.
- URL:
-
Publications:
hal-01344090, hal-01391578, hal-03105815, hal-03471095, hal-03516749, hal-03889276, hal-04713897, tel-04884651, hal-05128954, hal-05396788
-
Contact:
Sylvie Boldo
-
Participants:
Sylvie Boldo, François Clement, Micaela Mayero, Vincent Martin, 4 anonymous participants
-
Partners:
LIPN (Laboratoire d'Informatique de l'Université Paris Nord), UTC
7.1.11 Capla
-
Keywords:
Compilation, Programming language
-
Functional Description:
Capla is a safe domain-specific programming language dedicated to low-level computer algebra libraries. It aims at improving the confidence in libraries such as GMP or BLAS by supplying an appropriate way of writing them while guaranteeing memory and temporal safety of the generated code.
Capla’s compiler is mostly written in Coq and uses the CompCert compiler as a backend. The language’s semantics has been formalized in Coq and the compiler’s correctness (correspondence between the behavior of source and generated programs) has been proved in Coq as well as the safety of the language.
- Publications:
-
Contact:
Guillaume Melquiond
-
Participant:
2 anonymous participants
7.2 Open data
Toccata's Gallery of Verified Programs
-
Contributors:
Ali Ayad, Andrei Paskevich, Asma Tafat, Benedikt Becker, Christine Paulin-Mohring, Claire Dross, Claude Marché, Cláudio Belo Lourenço, Clément Fumex, François Bobot, Guillaume Melquiond, Jean-Christophe Filliâtre, Josué Moreau, Leon Gondelman, Léo Andrès, Martin Clochard, Mário Pereira, Nicolas Jeannerod, Paul Bonnot, Paul Patault, Quentin Garchery, Ran Chen, Raphaël Rieu-Helft, Romain Bardou, Sylvain Dailler, Sylvie Boldo, Thi Minh Tuyen Nguyen, Xavier Denis, Yannick Moy, Yuto Takei
-
Description:
This data set is a collection of programs formally verified, performed by tools developed in our team. The programs range from simple representative code, as good examples for teaching, to large case studies. These also include solutions to the successive VerifyThis challenges that appeared during the recent years.
- Project link:
-
Publications:
45, see also all references given inside the data set itself
-
Contact:
Claude Marché, Jean-Christophe Filliâtre
-
Release contributions:
The current version on the web is synchronised with Why3 version 1.8 released in December 2024
8 New results
8.1 Foundations and Spreading of Deductive Program Verification
Participants: Andrei Paskevich, Claude Marché, Guillaume Melquiond, Jean-Christophe Filliâtre, Léo Andrès, Sylvain Conchon, Paul Patault, Henri Saudubray, Matteo Manighetti.
Improving Verification Condition Generation
Filliâtre, Paskevich and Patault introduce Coma, a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers the user an additional degree of freedom, as they can provide separate specification (or none at all) for different execution paths. They define a verification condition generator for Coma and prove its correctness. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, the verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In addition, their procedure can factorise selected sub-goals on the fly, which leads to more compact verification conditions. They illustrate the use of Coma on two non-trivial examples, which have been formalised and verified using their implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code. An article presenting this work was presented at the ESOP Conference in 2025 17. An extended version is submitted for a journal-after publication in TOPLAS.
Paul Patault made a presentation of Coma at the Dafny workshop affiliated with POPL 2026 26. He is currently working on a Rocq formalization of the Coma language and its VC generator.
Automated Reasoning on Inductive Predicates
Filliâtre, Paskevich and Saudubray 66, 22 worked on an extension of the Why3 tool to allow proofs by induction on instances of inductive predicates, i.e. on finitely constructed derivations. It consists of a new matching construction to analyse the form of such a derivation, on the one hand, and a new notion of variant to justify the termination of a recursive function that proceeds according to the size of a derivation, on the other hand. They show how this extension can be implemented conservatively, with almost nothing changed in the verification condition generator of Why3. They illustrate the robustness of this contribution by translating from Coq to Why3 a non-trivial proof containing a large number of reasoning steps by induction on inductive predicates.
Cross-Language Symbolic Execution
One key problem in the field of software security is to expose software vulnerabilities effectively. Traditional testing methods have shown inadequacy in terms of path coverage and bug detection, due to their reliance on concrete input values. Hui and Andrès 16 proposed the idea of combining symbolic execution with run-time annotation checking. By using symbolic input values instead of concrete ones, the specified program properties can be checked on all the corner cases. They introduce two implementations of symbolic run-time annotation checkers: one for C, using the ANSI/ISO C Specification Language, and one for WebAssembly, using the Weasel specification language designed by them. Their approach combines the ease of use and the expressiveness of runtime annotation checking, as well as the power of program analysis.
8.2 Reasoning on mutable memory in program verification
Participants: Andrei Paskevich, Armaël Guéneau, Arnaud Golfouse, Claude Marché, Guillaume Melquiond, Jean-Christophe Filliâtre, Josué Moreau, Léo Andrès, Sylvain Conchon.
Reasoning with Memory Separation
Filliâtre and Paskevich proposed a technique for specifying and proving imperative programs manipulating pointer-based recursive data structures, which is better suited for first-order automated provers. The idea is to map recursive data structures, such as linked lists or trees, onto flat integer-indexed sequences, in such a way that separation and frame properties can be expressed using only simple arithmetic relations. This approach is illustrated with two examples: an original variant of list reversal and Morris's algorithm for constant-space traversal of a binary tree. This work was presented at iFM 2025 13.
Verification of Rust programs
One of the major success of Toccata during the last years is represented by the results obtained concerning the verification of Rust programs. Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification of Rust code. The project underlying the PhD thesis of Denis 61, supervised by J.-H. Jourdan and C. Marché, is to propose techniques for the verification of Rust program, using a translation to a purely-functional language. The challenge of this translation is the handling of mutable borrows: pointers which control of aliasing in a region of memory. To overcome this, we used a technique inspired by prophecy variables to predict the final values of borrows 62. This method is implemented in a standalone tool called Creusot 63. The specification language of Creusot features the notion of prophecy mentioned above, which is central for the specification of behaviour of programs performing memory mutation. However, so far, this prophecy-based encoding has only been described in the idealised setting of a core calculus.
Golfouse, Jourdan and Guéneau, in collaboration with Xavier Denis and Dominic Stolz 35 show how one might "scale" this technique up to the setting of a realistic verification tool. After describing why doing so is non-trivial, they show how to integrate this encoding with two common features of deductive verification systems: ghost code and type invariants. Additionally, they provide concrete implementation strategies for key aspects of the encoding that were unspecified but turn out to be crucial when considering realistic programs. They implemented this work as an extension of Creusot.
The type system of Rust enforces the "shared xor mutable" principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of interior mutability. Thus, supporting interior mutability in a deductive verification tool is difficult. The Verus tool demonstrated the use of ghost resources to that end. So far, this mechanism has only been applied to Verus in order to verify primarily system code. Arnaud Golfouse, Armaël Guéneau and Jacques-Henri Jourdan extended the deductive verification tool Creusot with support for linear ghost resources. They show how Creusot's full support for mutable borrows enables better specifications for primitives of linear ghost code. They apply this methodology to the verification of two data structures using sharing and mutation: union-find and persistent arrays 14. Later on, Golfouse and Patault formalised and verified a Rust code implementing a tree traversal with in-place mutation (algorithm due to Morris), again using the ghost ownership feature 15.
Inference of Specifications for Closures
In many programs, closures allow to express data transformations in a concise way. But when a verification tool is used, they must be accompanied by specifications that are often longer than their body. This is a particularly unpleasant problem, since these closures are often simple and their specification is redundant. Patault, Golfouse and Denis 18 presented a mechanism for inferring the specification of closures for the formal verification of Rust programs. They propose the use of the intermediate verification language Coma as a back-end for the deductive verification tool Creusot. Their design is able to manage the internal mutable state of a closure and to infer its specification. They use this mechanism to verify in an ergonomic and modular way a series of Rust programs using higher-order functions.
Safe Libraries for Computer Algebra
Low-level libraries used in computer algebra systems, such as GMP, BLAS/LAPACK, etc., are usually written in C, Fortran, and Assembly, and make heavy use of arrays and pointers. Melquiond and Moreau 75, 21, 27 have designed Capla, a programming language dedicated to writing such libraries. This language, halfway between C and Rust, is designed to be safe and to ease the deductive verification of programs, while being low-level enough to be suitable for this kind of computationally intensive applications. They have also written a compiler for this language, based on CompCert. The safety of the language has been formally proved using the Rocq proof assistant, and so has the property of semantics preservation for the compiler.
8.3 Verification of Computer Arithmetic
Participants: Claude Marché, David Hamelin, Guillaume Melquiond, Houda Mouhcine, Paul Bonnot, Paul Geneau de Lamarlière, Sylvie Boldo.
Reasoning about Floating-Point Programs
Numerical programs make use of the floating-point representation of numbers to perform computations that ideally should be done on mathematical real numbers. The floating-point representation induces approximations on the computations ultimately performed. We have a long tradition of study of subtle algorithms involving such numerical computations. A set of numerical programs that we studied is related to the combination of exponential and logarithm functions, that is, the log-sum-exp function known in the context of Machine Learning 76, for which Bonnot et al. 54 provide certified bounds on its accuracy. This work is extended this year to another function of the same shape, yet more complex, involving exponential of squares of differences, and summation of logarithms 32.
Boyer, Faissole, and Melquiond 55 have patented a method and system to transform a program, which includes mathematical functions applied to floating-point variables (and thus suffers from numerical approximations and rounding errors), in order to achieve a specified global accuracy.
Bonnot, Boyer, Faissole, and Marché 52 propose to bound the error between the computed result and the ideal computation by a formula involving the assumed precision of the input of the programs, together with the accuracy properties of the auxiliary mathematical functions that are called as basic blocks. Obtaining such an accuracy property needs a high expertise in floating-point computer arithmetic. The proposed methodology is able to automatically generate such form of accuracy formulas from a given input program. Moreover the generated formulas are certified correct with a high level of confidence, thanks to the automated construction of formal proofs of their validity. The methodology is implemented and experimented on several examples involving approximations of elementary functions such as sine, cosine, exponential and logarithm.
Writing a formal proof offers the highest possible confidence in the correctness of a mathematical library. This comes at a large cost though, since formal proofs require taking into account all the details, even the seemingly insignificant ones, which makes them tedious to write. Faissole, Geneau and Melquiond 65, 20 propose a methodology and some dedicated automation, and apply them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modelling of an external code, it is an actual floating-point function defined in the logic of the Rocq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20x speedup with respect to the previous implementation.
Given a program with floating-point computations, there are many analysis tools, available to obtain an upper bound on the rounding error. We aim to evaluate the tightness of this rounding bound by exhibiting input values for the program where the rounding error is close to this bound (called "pathological cases"). Boldo, Hamelin, Hilaire and Piriou 23 proposed an automatic method for generating pathological cases based on delta debugging and guided by Gappa. We have implemented this method and applied it to numerous examples from FPBench and publications.
The square root function and its variants are already hardware accelerated in most processors, including Kalray's where one square root function can be computed per cycle in the core. O. Desrentes 25 worked on a new accelerator-specific way of implementing the family of square root functions, using a mix of hardware and software accelerations. Hence a method to accelerate the reciprocal square root, the square root and the reciprocal function using one hardware operator based on multipartite tables, and software refinements as needed to fit the required accuracy target.
Formalization of Mathematics for Numerical Analysis
In her PhD thesis 77 defended in 2024, Houda Mouhcine presented results about the definition of finite elements and of the Lagrange simplicial finite elements, with the proof of their fundamental property called unisolvence. All the developments are distributed as part of the Coq-Num-Analysis library. The corresponding journal paper is currently under review 31, 30.
Moreover, this work lead to a comprehensive Rocq formalization of specific orders (namely monomial and graded) 28, 29, for the formalization of both monomials in dimension and Lagrange nodes that are evenly distributed on a simplex.
8.4 Spreading Formal Proofs
Participants: Andrei Paskevich, Claude Marché, David Hamelin, Florent Hivert, Guillaume Melquiond, Jean-Christophe Filliâtre, Josué Moreau, Léo Andrès, Sylvie Boldo.
Programmable Logic Controllers
Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. A long-term collaboration with MERCE as for goal the verification that a given Ladder program conforms to an expected behaviour expressed by a timing chart, describing a scenario of execution. This method relies on a modelling of Ladder programs in WhyML, the language of the Why3 environment for deductive program verification. This year, this work was extended to proving the conformity of a Ladder program with respect to a State Transition Diagram 34. Unlike timing charts, such a diagram can describe the complete set of expected execution scenarios.
Validation of Railway Data
In collaboration with B. Boyer from MERCE, N. Canva, M. Manighetti and C. Marché 33 presented the design, the formalisation and the implementation of a prototype software tool that checks whether a given constraint is valid on a given database representing a railway network. The underlying constraint language is able to express topological properties of the railway network. The semantics of constraints is formally defined and the implementation of the checker is formally proved to conform to that specification. The code is extracted to OCaml and compiled into an executable program, linked together with extra non verified code to import data from files. It is experimented on significantly complex examples, showing that the efficiency of the checker is satisfactory. Additionally, when a constraint is not checked valid, a counterexample is provided to exemplify why. Experimental results regarding counterexamples are satisfactory as well. This work will be presented at the next Dafny conference in January 2026 24.
Teaching Mathematics with Rocq
As part of the LiberAbaci défi, we work on how to use Rocq for teaching mathematics. In the past year we worked on worksheets in Rocq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). Boldo et al. 11 present technical and pedagogical choices, together with the numerous exercises they developed. As expected, it requires additional Rocq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.
Verifying Mathematics on a Large Scale
While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. As part of the ERC Fresco project, Hivert and Melquiond have designed a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large presentations from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations onto the Rocq formalization, so that the formal proofs could be checked in a reasonable amount of time 12.
Combinatorics and Data Structures.
J.-C. Filliâtre introduces an efficient data structure to implement small multisets, with an application to the enumeration of anagrams. This work has been successfully submitted to JFLA 2026 19 and will be presented in January 2026 at the conference.
In collaboration with V. Pilaud and L. Schwob, F. Hivert prove that the excedance relation on permutations defined by N. Bergeron and L. Gagnon actually extends to a congruence of the lattice on alternating sign matrices. Motivated by this example, they study 71 all lattice congruences of the lattice on alternating sign matrices whose quotient is isomorphic to the Stanley lattice on Dyck paths, which they call Catalan congruences. They prove that the maxima of the congruence classes are always covexillary permutations (and all covexillary permutations appear this way), and that the minimal permutations in each class are always precisely the 321-avoiding permutations. Finally, they show that any choice of representative permutations in each congruence class yield a basis of the Temperley–Lieb algebra with parameter 2, vastly generalising the bases arising from the excedance relation.
9 Bilateral contracts and grants with industry
9.1 ProofInUse-MERCE Collaboration
Participants: Claude Marché [contact], Guillaume Melquiond, Paul Bonnot, Noé Canva, Matteo Manighetti, Paul Geneau de Lamarlière.
This bilateral contract is part of the ProofInUse effort. This collaboration joins efforts of the Inria project-team Toccata and the company Mitsubishi Electric R&D (MERCE) in Rennes. It is funded by a bilateral contract of 6 years and 6 months from Nov 2019 to April 2026.
MERCE has strong and recognised skills in the field of formal methods. In the industrial context of the Mitsubishi Electric Group, MERCE has acquired knowledge of the specific needs of the development processes and meets the needs of the group in different areas of application by providing automatic verification and demonstration tools adapted to the problems encountered.
The objective of ProofInUse-MERCE is to significantly improve on-going MERCE tools regarding the verification of Programmable Logic Controllers and also regarding the verification of numerical C codes.
9.2 CIFRE contract with MERCE
Participants: Guillaume Melquiond [contact], Paul Geneau de Lamarlière.
Paul Geneau de Lamarlière started a CIFRE PhD in March 2023, under the supervision of Guillaume Melquiond and Florian Faissole at MERCE. It aims at the design of better proof environments for verifying programs with complex floating-point computations 65, 20.
9.3 CIFRE contract with EDF
Participants: Sylvie Boldo [contact], David Hamelin.
We have begun in December 2024 a collaboration with EDF by the CIFRE thesis of David Hamelin. The goals here are how to control rounding errors and to transport code from floating- to fixed-point arithmetic in the specific context of EDF qualified codes. We are interested in how to limit rounding errors in floating- and fixed-point code, how to determine different formats for each fixed-point calculation, and how to ensure there will be no overflow.
10 Partnerships and cooperations
10.1 European initiatives
10.1.1 H2020 projects
EMC2
EMC2 project on cordis.europa.eu
-
Title:
Extreme-scale Mathematically-based Computational Chemistry
-
Duration:
From September 1, 2019 to August 31, 2026
-
Partners:
- INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET AUTOMATIQUE (INRIA), France
- ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE (EPFL), Switzerland
- ECOLE NATIONALE DES PONTS ET CHAUSSEES (ENPC), France
- CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE CNRS (CNRS), France
- SORBONNE UNIVERSITE, France
-
Inria contact:
Laura GRIGORI (Alpines)
- Coordinator:
-
Summary:
Molecular simulation has become an instrumental tool in chemistry, condensed matter physics, molecular biology, materials science, and nanosciences. It will allow to propose de novo design of e.g. new drugs or materials provided that the efficiency of underlying software is accelerated by several orders of magnitude.
The ambition of the EMC2 project is to achieve scientific breakthroughs in this field by gathering the expertise of a multidisciplinary community at the interfaces of four disciplines: mathematics, chemistry, physics, and computer science. It is motivated by the twofold observation that, i) building upon our collaborative work, we have recently been able to gain efficiency factors of up to 3 orders of magnitude for polarizable molecular dynamics in solution of multi-million atom systems, but this is not enough since ii) even larger or more complex systems of major practical interest (such as solvated biosystems or molecules with strongly-correlated electrons) are currently mostly intractable in reasonable clock time. The only way to further improve the efficiency of the solvers, while preserving accuracy, is to develop physically and chemically sound models, mathematically certified and numerically efficient algorithms, and implement them in a robust and scalable way on various architectures (from standard academic or industrial clusters to emerging heterogeneous and exascale architectures).
EMC2 has no equivalent in the world: there is nowhere such a critical number of interdisciplinary researchers already collaborating with the required track records to address this challenge. Under the leadership of the 4 PIs, supported by highly recognized teams from three major institutions in the Paris area, EMC2 will develop disruptive methodological approaches and publicly available simulation tools, and apply them to challenging molecular systems. The project will strongly strengthen the local teams and their synergy enabling decisive progress in the field.
FRESCO, ERC Consolidator project
Participants: Florent Hivert, Guillaume Melquiond, Josué Moreau.
-
Title:
Fast and Reliable Symbolic Computation
-
Duration:
November 2021 – October 2027
-
Coordinator:
Assia Mahboubi (Gallinette)
- Website:
Using computers to formulate conjectures and consolidate proof steps pervades all mathematics fields, even the most abstract. Most computer proofs are produced by symbolic computations, using computer algebra systems. However, these systems suffer from severe, intrinsic flaws, rendering computational correction and verification challenging. The FRESCO project aims to shed light on whether computer algebra could be both reliable and fast. Researchers will disrupt the architecture of proof assistants, which serve as the best tools for representing mathematics in silico, enriching their programming features while preserving their compatibility with their logical foundations. They will also design novel mathematical software that should feature a high-level, performance-oriented programming environment for writing efficient code to boost computational mathematics.
10.2 National initiatives
10.2.1 ANR NuSCAP
Participants: Guillaume Melquiond [contact], Sylvie Boldo.
The last twenty years have seen the advent of computer-aided proofs in mathematics and this trend is getting more and more important. They request various levels of numerical safety, from fast and stable computations to formal proofs of the computations. Hovewer, the necessary tools and routines are usually ad hoc, sometimes unavailable, or inexistent. On a complementary perspective, numerical safety is also critical for complex guidance and control algorithms, in the context of increased satellite autonomy. We plan to design a whole set of theorems, algorithms and software developments, that will allow one to study a computational problem on all (or any) of the desired levels of numerical rigor. Key developments include fast and certified spectral methods and polynomial arithmetic, with subsequent formal verifications. There will be a strong feedback between the development of our tools and the applications that motivate it.
The project led by École Normale Supérieure de Lyon (LIP) has started in February 2021 and lasts for 4 years. Partners: Inria (teams Aric, Galinette, Lfant, Marelle, Toccata), École Polytechnique (LIX), Sorbonne Université (LIP6), Université Sorbonne Paris Nord (LIPN), CNRS (LAAS).
10.2.2 ANR GOSPEL
Participants: Jean-Christophe Filliâtre [contact], Andrei Paskevich, Armaël Guéneau, Paul Patault.
A specification language extends a programming language by allowing code and specifications to be written in a single document. Examples include SparkAda, JML, and ACSL, which extend Ada, Java, and C with syntax for specifications.
By offering a specification language to programmers, one encourages them to document, test, and verify their code as they write it, not as a separate step that is too easily postponed. From a technical point of view, the presence of specifications makes it possible to test or verify each module independently and is the key to scalability. From a pragmatic point of view, embedding specifications in the code allows them to be automatically distributed (via a package management system) to every programmer; this is the key to practical adoption.
The GOSPEL project proposes to develop Gospel, a specification language that extends the programming language OCaml; to develop an ecosystem of tools based on Gospel; and to demonstrate and validate these tools via several case studies.
The project led by Inria Paris has started in October 2022 and lasts for 4 years. Partners: Inria Paris (team Cambium), Université Paris-Saclay (LMF), Tarides, Nomadic Labs.
10.2.3 Project “SecurEval” of PEPR Cybersécurité
Participants: Sylvain Conchon [contact].
The SecureVal project aims to design new tools, benefiting from new digital technologies, to verify the absence of hardware and software vulnerabilities, and carry out the proof of compliance required.
In order to deal effectively with modern digital systems, code analysis techniques, which originated in the world of critical systems, must be overhauled to adapt to the objectives of security assessments and to scale up to complex systems, combining dedicated functionalities and third-party libraries. For example, the design of new fault models, the support of emerging languages, the visualization of formal guarantees, the use of learning techniques to automate repetitive actions or optimize the extraction of relevant information, or the development of approaches combining static and dynamic analyses.
The project is led by CEA-List, it started in 2022 and lasts for 6 years.
10.2.4 Project I-Demo “Décysif”
Participants: Andrei Paskevich, Armaël Guéneau, Claude Marché [contact], Jean-Christophe Filliâtre, Sylvain Conchon, Li-Yao Xia, Arnaud Golfouse, Maël Coulmance, Vincent Lafeychine, Jacques-Henri Jourdan, Paul Patault.
The Décysif project is a project started in december 2023, for 4 years. Its general goal is the promotion of formal verification for critical systems regarding cybersecurity. This project will fund our future research on Rust program verification, and it contains a workpackage dedicated towards industrialization of the Creusot tool.
The project is led by TrustInSoft company, with AdaCore and OCamlPro as other partners.
10.2.5 Inria Project LiberAbaci
Participants: Sylvie Boldo [contact].
The Défi Inria LiberAbaci is a collaborative project aimed at improving the accessibility of the Coq interactive proof system for an audience of mathematics students in the early academic years.
The head is Yves Bertot and the involved teams are: Cambium (Paris), Camus (Strasbourg), Gallinette (Nantes) PiCube (Paris), Spades (Grenoble), Stamp (Sophia Antipolis), Toccata (Saclay), LIPN (Villetaneuse).
11 Dissemination
Participants: Andrei Paskevich, Armaël Guéneau, Claude Marché, Guillaume Melquiond, Jean-Christophe Filliâtre, Josué Moreau, Paul Geneau de Lamarlière, Sylvain Conchon, Sylvie Boldo.
11.1 Promoting scientific activities
11.1.1 Scientific events: selection
Chair of conference program committees
- G. Melquiond, 32nd IEEE International Symposium on Computer Arithmetic, ARITH'2025.
Member of the conference program committees
- S. Boldo, 32nd IEEE Symposium on Computer Arithmetic, ARITH'2025
- S. Boldo, 17th NASA Formal Methods Symposium, NFM'2025
- S. Boldo, Certified Programs and Proofs Symposium, CPP'2025
- S. Boldo, Certified Programs and Proofs Symposium, CPP'2026
- S. Boldo, Rocqshop 2025
- S. Boldo, International Workshop on Verification of Scientific Software, VSS 2025
- J.-C. Filliâtre, 17th NASA Formal Methods Symposium, NFM'2025
- G. Melquiond, ACM SIGPLAN International Conference on Functional Programming, ICFP 2025.
- G. Melquiond, Journées Francophones des Langages Applicatifs, JFLA 2026.
- A. Paskevich, 19th International Symposium on Theoretical Aspects of Software Engineering, TASE 2025
- A. Paskevich, 17th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2025
11.1.2 Journal
Member of the editorial boards
- S. Boldo: member of the editorial board of IEEE Transactions on Emerging Topics in Computing (TETC), since 2023.
- J.-C. Filliâtre: member of the editorial board of the Journal of Functional Programming, since 2011.
- J.-C. Filliâtre: member of the editorial board of the journal Formal Aspects of Computing, since 2021.
- A. Paskevich, member of the editorial board of Formal Methods in System Design, since 2021.
- G. Melquiond: member of the editorial board of Reliable Computing, since 2019.
11.1.3 Invited talks
- S. Boldo, invited speaker at the inaugural session of the maths-computer science master of Toulon, September 12, 2025.
- S. Boldo, invited speaker at the Europroofnet Symposium 2025 on Proof Libraries, September 16 2025, Orsay.
- S. Boldo, invited speaker at the RAIM 2025 “16th Rencontres de l'Arithmétique en Informatique Mathématique – A Tribute to Jean-Michel Muller”, November 5 2025, Lyon.
- J.-C. Filliâtre, invited speaker at Algorithmique et programmation, May 5–9, 2025, Luminy.
11.1.4 Leadership within the scientific community
- S. Boldo, elected chair of the ARITH working group of the GDR-IM (a CNRS subgroup of computer science) with L.-S. Didier (Université Toulon).
- S. Boldo, steering committee member of the IEEE International Symposium on Computer Arithmetic.
- S. Boldo, elected board steering committee member of the IEEE International Symposium on Computer Arithmetic, since 2025.
- J.-C. Filliâtre, steering committee member of JFLA (Journées Francophones des Langages Applicatifs).
- J.-C. Filliâtre, member of IFIP WG 1.9/2.15 Verified Software.
- G. Melquiond, steering committee member of the IEEE International Symposium on Computer Arithmetic.
11.1.5 Scientific expertise
- S. Boldo and J.-C. Filliâtre, (local) members of the LMF scientific council.
- S. Boldo, member of the ENSIIE scientific council.
- J.-C. Filliâtre, member of the recruitment committee of an associate professor position at LIP6, Sorbonne Université.
- C. Marché, grading the entrance examination at X/ENS (“option informatique”).
- F. Hivert, president of the recruitment committee of an associate professor position at PolyTech, Université Paris-Saclay.
- C. Marché, A. Paskevich, members of the recruitment committee of an associate professor position at PolyTech, Université Paris-Saclay.
- G. Melquiond, member of the recruitment committee of a professor position at École Normale Supérieure Paris-Saclay.
- A. Paskevich, member of the recruitment committee of an associate professor position at EPISEN, Université Paris-Est Créteil.
11.1.6 Research administration
- S. Boldo, president of the concours de l'agrégation d'informatique, 2022-2025.
- J.-C. Filliâtre, leader of the Proof and Languages department of LMF.
- A. Guéneau, member of the Commission des Utilisateurs des Moyens Informatiques of Inria Saclay.
- A. Guéneau, member of the Commission de Développement Technologique of Inria Saclay.
- G. Melquiond, member of the Bureau du Comité des Projets of Inria Saclay.
- G. Melquiond, member of the Commission Consultative de l'Université Paris-Saclay (section 27).
- G. Melquiond, member of the Conseil de Politique Doctorale of Université Paris-Saclay.
- G. Melquiond, member of the doctoral school STIC of Université Paris-Saclay.
- G. Melquiond, member of the Mission Jeunes Chercheurs of Inria.
- G. Melquiond, member of the laboratory council of LMF.
- G. Melquiond, leader of the team Computer Arithmetic of LMF.
- A. Paskevich, leader of the team Program Verification of LMF.
11.2 Teaching - Supervision - Juries - Educational and pedagogical outreach
11.2.1 Teaching
- J.-C. Filliâtre, Langages de programmation et compilation, 25h, L3, École Normale Supérieure, France.
- J.-C. Filliâtre, Les bases de l'algorithmique et de la programmation, 15h, L3, École Polytechnique, France.
- J.-C. Filliâtre, Compilation, 18h, M1, École Polytechnique, France.
- A. Guéneau, Programmation avancée, 12h, L3, ENS Paris-Saclay, France.
- A. Paskevich, Vérification Déductive, 12h, M2, MPRI, Université Paris Cité, France.
- A. Paskevich, Programmation système, 56h, BUT2, IUT d'Orsay, Université Paris-Saclay, France.
11.2.2 Supervision
- PhD: J. Moreau, “Programming language and formally verified compiler for low-level numerical libraries”, since Oct. 2022, supervised by G. Melquiond. Defended in Nov. 2025 27.
- PhD in progress: P. Geneau de Lamarlière, “Design of formally verified floating-point components”, since Sep. 2022, supervised by G. Melquiond.
- PhD in progress: A. Golfouse, “Vérification de programme Rust avancée: invariants de types, code fantôme, possession fantôme et algèbre de ressources, concurrence et aliasing”, since Oct. 2023, supervised by J.-H. Jourdan and A. Guéneau.
- PhD in progress: P. Patault, “Conception et étude d'un langage de programmation adapté à la vérification déductive”, since Oct. 2023, supervised by J.-C. Filliâtre and A. Paskevich.
- PhD in progress: D. Hamelin, “Implémentation de calculs numériques en virgule fixe avec maîtrise de l’erreur d’arrondi.”, since Dec. 2024, supervised by S. Boldo, T. Hilaire (Sorbonne University) and P.-Y. Piriou (EDF).
- PhD in progress: V. Lafeychine, “Prise en compte des comportements mémoire relâchés dans l'outil de vérification déductive pour Rust Creusot”, since Sep. 2025, supervised by C. Marché and J.-H. Jourdan (LMF).
- PhD in progress: H. Saudubray, “Conception et unification des langages de programmation, spécification et preuve dans le contexte de la vérification déductive de programmes, au sein de l'outil Why3”, since Oct. 2025, supervised by J.-C. Filliâtre and A. Paskevich.
- M2 internship: S. Shrivastava, “Automatisations en Rocq”, April-August 2025, supervised by S. Boldo, F. Clément (Inria Paris), and M. Mayero (Sorbonne Paris-Nord).
- M2 internship: V. Lafeychine, “Modèle sémantique de Creusot : places, code fantôme, invariants de type”, March-August 2025, supervised by J.-H. Jourdan and A. Guéneau.
11.2.3 Juries
- S. Boldo, president of the PhD jury of Valentin Dardilhac, “Mécanismes de votes et résolutions de systèmes d'inéquations à variables réelles”, July 16, 2025, Université Paris-Saclay.
- S. Boldo, president of the PhD jury of Sylvain Joube, “Performance Portable pour le Calcul à Haut Débit”, October 9, 2025, Université Paris-Saclay.
- S. Boldo, member of the HDR jury of Pierre Roux, “Numerical Computations and Proofs: from Proof-Assistants to Aerospace Applications”, December 1, 2025, Toulouse.
- S. Conchon, reviewer of the PhD thesis of Hector Suzanne, “Reusable static resource analyses for high level languages”, 2025, Sorbonne université.
- S. Conchon, president of the PhD jury of Hichem Rami Ait El Hara, “Theory of sequences tailored for program verification”, 2025, Université Paris-Saclay.
- J.-C. Filliâtre, reviewer of the PhD thesis of S. La Spina, Dec 16, 2025, Université Rennes.
- J.-C. Filliâtre, reviewer of the PhD thesis of A. Reitz, Dec 5, 2025, Inria Paris.
- C. Marché, president of the PhD jury of Yani Ziani, “Vérification formelle de couches de confiance dans les logiciels : application à la TPM Software Stack”, October 9, 2025, Université d'Orléans.
11.3 Popularization
11.3.1 Participation in Live events
- S. Boldo has lead a session for ninth grade trainees (stagiaires de 3ème) on December 19, 2025.
- J.-C. Filliâtre has lead a session for ninth grade trainees (stagiaires de 3ème) on December 17, 2025.
12 Scientific production
12.1 Major publications
- 1 articleThe CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages.International Journal on Software Tools for Technology Transfer2022HALback to text
- 2 articleAutomated Formal Analysis of Temporal Properties of Ladder Programs.International Journal on Software Tools for Technology Transfer2462022, 977-997HALDOIback to text
- 3 articleA Coq Formalization of Lebesgue Integration of Nonnegative Functions.Journal of Automated Reasoning662022, 175–213HALDOIback to text
- 4 articleFloating-point arithmetic.Acta Numerica32May 2023, 203-290HALDOIback to text
- 5 articleDeclarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker.Fundamenta Informaticae1784February 2021, 347-378HALDOIback to text
- 6 inproceedingsThe Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker.Lecture Notes in Computer ScienceSEFM 2023 - Software Engineering and Formal MethodsLNCS-14323Software Engineering and Formal MethodsEindhoven, NetherlandsSpringer Nature SwitzerlandOctober 2023, 30-46HALDOIback to text
- 7 inproceedingsAbstraction and Genericity in Why3.ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation12476Rhodes, Greece2020HALDOIback to text
- 8 articleCerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.Journal of the ACM (JACM)September 2023HALDOIback to text
- 9 inproceedingsRustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code.PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and ImplementationSan Diego CA USA, United StatesACMJune 2022, 841-856HALDOIback to text
- 10 articleWhyMP, a Formally Verified Arbitrary-Precision Integer Library.Journal of Symbolic Computation115March 2023, 74-95HALDOIback to text
12.2 Publications of the year
International peer-reviewed conferences
National peer-reviewed Conferences
Conferences without proceedings
Doctoral dissertations and habilitation theses
Reports & preprints
Other scientific publications
12.3 Cited publications
- 37 miscNVIDIA: Adoption of SPARK Ushers in a New Era in Security-Critical Software Development.2023back to text
- 38 inproceedingsMulti-Prover Verification of Floating-Point Programs.Fifth International Joint Conference on Automated Reasoning6173Lecture Notes in Artificial IntelligenceEdinburgh, ScotlandSpringerJuly 2010, 127--141URL: http://hal.inria.fr/inria-00534333back to text
- 39 bookNumérique et Sciences Informatiques, 24 leçons avec exercices corrigés. Terminale.Ellipses2020, URL: https://hal.inria.fr/hal-03023099back to text
- 40 bookNumérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Première..Ellipses2019, URL: https://inria.hal.science/hal-02379073back to text
- 41 bookInformatique - MP2I/MPI - CPGE 1re et 2e années - Cours et exercices corrigés.Ellipses2022, URL: https://hal.inria.fr/hal-03886751back to text
- 42 inproceedingscvc5: A Versatile and Industrial-Strength SMT Solver.Tools and Algorithms for the Construction and Analysis of Systems13243Lecture Notes in Computer ScienceSpringer2022, 415--442back to text
- 43 inproceedingsMETEOR : A successful application of B in a large project.Proceedings of FM'99: World Congress on Formal MethodsLecture Notes in Computer Science (Springer-Verlag)Springer VerlagSeptember 1999, 369--387back to text
- 44 inbookGuide to Software Verification with Frama-C --- Core Components, Usages, and Applications.Springer-Verlag2024, Formally Expressing what a Program Should Do: the ACSL Language3--80URL: https://inria.hal.science/hal-04265707back to text
- 45 articleLet's Verify This with Why3.International Journal on Software Tools for Technology Transfer (STTT)1762015, 709--727HALback to textback to text
- 46 inproceedingsFormal Proof of a Wave Equation Resolution Scheme: the Method Error.Interactive Theorem Proving6172Lecture Notes in Computer ScienceSpringer2010, 147--162URL: http://hal.inria.fr/inria-00450789/enback to text
- 47 articleWave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program.Journal of Automated Reasoning504April 2013, 423--456URL: http://hal.inria.fr/hal-00649240/en/back to text
- 48 inproceedingsCombining Coq and Gappa for Certifying Floating-Point Programs.16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning5625Lecture Notes in Artificial IntelligenceGrand Bend, CanadaSpringerJuly 2009, 59--74back to text
- 49 articleFormal verification of numerical programs: from C annotated programs to mechanical proofs.Mathematics in Computer Science542011, 377--393URL: http://hal.inria.fr/hal-00777605back to textback to text
- 50 bookComputer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System.ISTE Press - ElsevierDecember 2017, URL: https://hal.inria.fr/hal-01632617back to text
- 51 articleProofs of numerical programs when the compiler optimizes.Innovations in Systems and Software Engineering722011, 151--160URL: http://hal.inria.fr/hal-00777639back to text
- 52 techreportGenerating and Certifying Accuracy Properties of Floating-Point Programs.RR-9564Inria2024, URL: https://inria.hal.science/hal-04820735back to text
- 53 techreportFormally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions.9531Inria2023, URL: https://inria.hal.science/hal-04343157back to text
- 54 inproceedingsFormally Verified Rounding Errors of the Logarithm-Sum-Exponential Function.Formal Methods in Computer-Aided DesignIEEE2024, URL: https://inria.hal.science/hal-04674600back to textback to text
- 55 techreportMethod and system for converting an input computer program into an output computer program achieving a target global accuracy.Patent number EP42353972024, URL: https://hal.science/hal-04872869back to text
- 56 articleAn overview of JML tools and applications.International Journal on Software Tools for Technology Transfer (STTT)73June 2005, 212--232back to text
- 57 inproceedingsDeductive Verification with Ghost Monitors.Principles of Programming LanguagesNew Orleans, United States2020, URL: https://hal.inria.fr/hal-02368284back to text
- 58 inproceedingsAlt-Ergo 2.2.SMT Workshop: International Workshop on Satisfiability Modulo TheoriesOxford, United KingdomJuly 2018HALback to text
- 59 bookApprendre à programmer avec OCaml. Algorithmes et structures de données.EyrollesSeptember 2014, 429URL: http://hal.inria.fr/hal-01063853back to text
- 60 inproceedingsA Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT.Computer Aided Verification10427Lecture Notes in Computer Science2017, 419--435URL: https://hal.inria.fr/hal-01522770back to text
- 61 phdthesisDeductive Verification of Rust Programs.Université Paris-Saclay2023, URL: https://hal.science/tel-04517581back to text
- 62 techreportDeductive program verification for a language with a Rust-like typing discipline.Université de ParisSeptember 2020, URL: https://hal.archives-ouvertes.fr/hal-02962804back to text
- 63 inproceedingsCreusot: a Foundry for the Deductive Verication of Rust Programs.International Conference on Formal Engineering Methods - ICFEMLecture Notes in Computer ScienceMadrid, SpainSpringer2022, URL: https://hal.inria.fr/hal-03737878back to text
- 64 articleCertifying the floating-point implementation of an elementary function using Gappa.IEEE Transactions on Computers6022011, 242--253URL: http://hal.inria.fr/inria-00533968/en/back to text
- 65 inproceedingsEnd-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation.5th International Conference on Interactive Theorem Proving309Tbilisi, GeorgiaLeibniz International Proceedings in Informatics2024, 14:1-14:18URL: https://hal.science/hal-04515714back to textback to text
- 66 inproceedingsProofs on Inductive Predicates in Why3.Big Specification: Specification, Proof, and Testing at ScaleCambridge, UKOctober 2024, URL: https://hal.science/hal-04734466back to text
- 67 techreportAutomated Verification of Floating-Point Computations in Ada Programs.RR-9060InriaApril 2017, 53URL: https://hal.inria.fr/hal-01511183back to text
- 68 inproceedingsAutomating the Verification of Floating-Point Programs.Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTELecture Notes in Computer Science10712Heidelberg, GermanySpringerDecember 2017, URL: https://hal.inria.fr/hal-01534533/back to text
- 69 inproceedingsOpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case.Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part IChamSpringer International Publishing2015, 273--289back to text
- 70 inproceedingsMelocoton: A Program Logic for Verified Interoperability Between OCaml and C.Object-Oriented Programming, Systems, Languages & ApplicationsACM2023, URL: https://inria.hal.science/hal-04203298back to text
- 71 miscHeaps of Rhombic Dodecahedra, Catalan Congruences on Alternating Sign Matrices, and Bases of the Temperley-Lieb Algebra.2025back to text
- 72 articleseL4: Formal verification of an OS kernel.Communications of the ACM536June 2010, 107--115back to text
- 73 articleA formally verified compiler back-end.Journal of Automated Reasoning4342009, 363--446URL: http://hal.inria.fr/inria-00360768/en/back to text
- 74 articleFormally Verified Approximations of Definite Integrals.Journal of Automated Reasoning622February 2019, 281--300URL: https://hal.inria.fr/hal-01630143back to text
- 75 inproceedingsA Safe Low-level Language for Computer Algebra and its Formally Verified Compiler.29th ACM SIGPLAN International Conference on Functional Programming8ICFPMilan, Italy2024, 121--146URL: https://inria.hal.science/hal-04485670back to text
- 76 inproceedingsThe Power of Log-Sum-Exp: Sequential Density Ratio Matrix Estimation for Speed-Accuracy Optimization.International Conference on Machine Learning139Proceedings of Machine Learning Research2021, 7792--7804URL: https://proceedings.mlr.press/v139/miyagawa21a.htmlback to text
- 77 phdthesisFormal Proofs in Applied Mathematics: A Coq Formalization of Simplicial Lagrange Finite Elements.Université Paris-Saclay2024, URL: https://theses.hal.science/tel-04884651back to text
- 78 inproceedingsZ3, An Efficient SMT Solver.TACAS4963Lecture Notes in Computer ScienceSpringer2008, 337--340back to text
- 79 bookHandbook of Floating-point Arithmetic (2nd edition).Birkhäuser BaselJuly 2018HALback to text
- 80 inproceedingsHardware-Dependent Proofs of Numerical Programs.Certified Programs and ProofsLecture Notes in Computer ScienceSpringerDecember 2011, 314--329URL: http://hal.inria.fr/hal-00772508back to text
- 81 inproceedingsCameleer: A Deductive Verification Tool for OCaml.Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II12760Lecture Notes in Computer ScienceSpringer2021, 677--689back to text
- 82 inproceedingsThunks and Debits in Separation Logic with Time Credits.POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages8SIGPLANACM2024, URL: https://hal.science/hal-04238691back to text
- 83 articleA Why3 proof of GMP algorithms.Journal of Formalized Reasoning2019, URL: https://inria.hal.science/hal-02477578back to text