VERIDIS

VERIDIS - 2025

2025Activity reportTeamVERIDIS

RNSR: 201020692C

Research‌ center Inria Centre at Université de Lorraine
In‌ partnership with:CNRS, Université de Lorraine, Max-Planck-Institut für‌ Informatik Saarbrücken
Team name: Modeling and Verification of‌ Distributed Algorithms and Systems
In collaboration with:Laboratoire‌ lorrain de recherche en informatique et ses applications‌ (LORIA)

Creation of the Team: 2025 January 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.7. Distributed programming
A2.1.11. Proof‌ languages
A2.2. Compilation
A2.5. Software engineering
A4.5. Formal‌ method for verification, reliability, certification
A4.5.1. Static analysis‌
A4.5.2. Model-checking
A4.5.3. Program proof
A7.2. Logic in‌ Computer Science
A8.4. Computer Algebra

1‌ Team members, visitors, external collaborators

Research Scientists

Stephan‌ Merz [Team leader, INRIA, Senior‌ Researcher, HDR]
Christoph Weidenbach [Team‌ leader, Max Planck Society, Senior Researcher‌, HDR]
Engel Lefaucheux [INRIA,‌ ISFP]
Thomas Sturm [CNRS, Senior‌ Researcher, HDR]
Sophie Tourret [INRIA‌, Researcher]
Uwe Waldmann [Max Planck‌ Society, Senior Researcher]

Faculty Members

Julie‌ Cailler [UL, Associate Professor]
Horatiu‌ Cirstea [UL, Professor, HDR]‌
Marie Duflot-Kremer [UL, Associate Professor]‌
Pierre-Etienne Moreau [UL, Professor, HDR‌]
Dominique Méry [UL, Professor,‌ HDR]
Sorin Stratulat [UL, Associate‌ Professor, HDR]
Martin Vassor [UL‌, Associate Professor]

Post-Doctoral Fellow

Qi Qiu‌ [UL, from Oct 2025, ATER‌]

PhD Students

Thomas Bagrel [UL, CIFRE, until Nov‌ 2025, Tweag]‌
Ghilain Bergeron [INRIA‌‌]
Yasmine Briefs [Max Planck Society,‌ from Apr 2025]‌
Alessio Coltellacci [INRIA‌‌]
Sarah Depernet [INRIA]
Martin Desharnais‌ [Max Planck Society‌, until Jan 2025‌‌]
Florent Krasnopol [UL, from Sep‌ 2025]
Hendrik Leidinger‌ [Max Planck Society‌‌, until Jun 2025]
Lorenz Leutgeb [‌Max Planck Society]‌
Simon Schwarz [Max‌‌ Planck Society]
Mohamed Amine Snoussi [UL‌, CIFRE, until‌ Aug 2025, Westinghouse‌‌]
Vincent Trélat [INRIA]

Interns and‌ Apprentices

Volkan Burakcin [‌INRIA, Intern,‌‌ from Jun 2025 until Jul 2025]
Tiago‌ Campos Ferreira [UL‌, Intern, from‌‌ Oct 2025]
Baptiste Diedler [INRIA,‌ Intern, from Jun‌ 2025 until Jul 2025‌‌]
Titouan Le Pen [UL, Intern‌, from May 2025‌ until Jun 2025]‌‌
Bastien Pichet [INRIA, Intern, from‌ May 2025 until Jun‌ 2025]
Achille Razafimaharo‌‌ [UL, Intern, from May 2025‌ until Jun 2025]‌
Lucas Villaume [UL‌‌, Intern, from Apr 2025 until Aug‌ 2025]

Administrative Assistants‌

Emmanuelle Deschamps [INRIA‌‌]
Elsa Maroko [CNRS]
Jennifer Müller‌ [Max Planck Society‌]
Cecilia Olivier [‌‌INRIA]

External Collaborator

Pascal Fontaine [ULIEGE‌, HDR]

2‌ Overall objectives

The VeriDis‌‌ project team includes members of the Formal Methods‌ department at LORIA, the‌ computer science laboratory in‌‌ Nancy, and members of the research group Automation‌ of Logic at Max‌ Planck Institut für Informatik‌‌ in Saarbrücken. It is headed by Stephan Merz‌ and Christoph Weidenbach. VeriDis‌ was created in 2010‌‌ as a local research group of Inria Nancy‌ – Grand Est and‌ has been an Inria‌‌ project team since July 2012.

The objectives of‌ VeriDis are to contribute‌ to advances in verification‌‌ techniques, including automated and interactive theorem proving, and‌ to make them available‌ for the development and‌‌ analysis of concurrent and distributed algorithms and systems,‌ based on mathematically precise‌ and practically applicable development‌‌ methods. The techniques that we develop are intended‌ to assist designers of‌ algorithms and systems in‌‌ carrying out formally verified developments, where proofs of‌ relevant properties, as well‌ as bugs, can be‌‌ found with a high degree of automation.

Within‌ this context, we work‌ on techniques for automated‌‌ theorem proving for expressive languages based on first-order‌ logic, with support for‌ theories (including fragments of‌‌ arithmetic or of set theory) that are relevant‌ for specifying algorithms and‌ systems. Ideally, systems and‌‌ their properties would be specified using high-level, expressive‌ languages, errors in specifications‌ would be discovered automatically,‌‌ and finally, full verification could also be performed‌ completely automatically. Due to‌ the fundamental undecidability of‌‌ the problem, this cannot be achieved in general.‌ Nevertheless, we have observed‌ important advances in automated‌‌ deduction in recent years,‌ to which we have contributed. These advances suggest‌ that a substantially higher degree of automation can‌ be achieved over what is available in today's‌ tools supporting deductive verification. Our techniques are developed‌ within trail-based solving and saturation-based reasoning, the two‌ main frameworks of contemporary automated reasoning, of which‌ respectively SMT (Satisfiability Modulo Reasoning) and superposition are‌ the current most prominent examples in first- and‌ higher-order logic. These two frameworks have complementary strengths‌ and weaknesses. Figuring out how and when to‌ make them converge is part of our interests.‌ Techniques developed within the symbolic computation domain, such‌ as algorithms for quantifier elimination for appropriate theories,‌ are also relevant, and are part of our‌ portfolio of techniques. In order to handle expressive‌ input languages, we are working on techniques that‌ encompass tractable fragments of higher-order logic, for example‌ for specifying inductive or co-inductive data types, for‌ automating proofs by induction, or for handling collections‌ defined through a characteristic predicate.

Since full automatic‌ verification remains elusive, another line of our research‌ targets interactive proof platforms. We intend these‌ platforms to benefit from our work on automated‌ deduction by incorporating powerful automated backends and thus‌ raise the degree of automation beyond what current‌ proof assistants can offer. Since most conjectures stated‌ by users are initially wrong (due to type‌ errors, omitted hypotheses or overlooked border cases), it‌ is also important that proof assistants be able‌ to detect and explain such errors rather than‌ letting users waste considerable time in futile proof‌ attempts. Moreover, increased automation must not come at‌ the expense of trustworthiness: skeptical proof assistants expect‌ to be given an explanation of the proof‌ found by the backend prover that they can‌ certify.

Model checking is an established and highly‌ successful technique for verifying systems and for finding‌ errors. Our contributions in this area more specifically‌ target quantitative aspects, in particular the verification of‌ timed or probabilistic systems. A specificity of VeriDis‌ is to consider partially specified systems, using parameters‌, in which case the verification problem becomes‌ the synthesis of suitable parameter valuations.

Our methodological‌ and foundational research is accompanied by the development‌ of efficient software tools, several of which‌ go beyond pure research prototypes: they have been‌ used by others or have been integrated in‌ verification platforms developed by other groups. We also‌ validate our work on verification techniques by applying‌ them to the formal development of algorithms and‌ systems. We mainly target high-level descriptions of‌ concurrent and distributed algorithms and systems. This class‌ of algorithms is ubiquitous, ranging from multi- and‌ many-core algorithms to large networks and cloud computing,‌ and their formal verification is notoriously difficult. Targeting‌ high levels of abstraction allows the designs of‌ such systems to be verified before an actual‌ implementation has been developed, contributing to reducing the‌ costs of formal verification. The potential of distributed‌ systems for increased resilience to component failures makes them attractive in many‌ contexts, but also makes‌ formal verification even more‌‌ important and challenging. Our work in this area‌ aims at identifying classes‌ of algorithms and systems‌‌ for which we can provide guidelines and identify‌ patterns of formal development‌ that makes verification less‌‌ an art and more an engineering discipline. We‌ mainly target components of‌ operating systems, distributed and‌‌ cloud services, and networks of computers or mobile‌ devices. When correctness properties‌ have been formally verified‌‌ for a high-level specification of an algorithm, the‌ correctness of an implementation‌ of an algorithm still‌‌ remains to be checked, using techniques such as‌ refinement proofs, code generation,‌ testing or trace validation.‌‌

Beyond formal system verification, we pursue applications of‌ some of the symbolic‌ techniques that we develop‌‌ in other domains. We have observed encouraging success‌ in using techniques of‌ symbolic computation for the‌‌ qualitative analysis of biological and chemical networks described‌ by systems of ordinary‌ differential equations that were‌‌ previously only accessible to large-scale simulation. Such networks‌ include biological reaction networks‌ as they occur with‌‌ models for diseases such as diabetes or cancer.‌ They furthermore include epidemic‌ models such as variants‌‌ and generalizations of SEIR1 models, which are‌ typically used for Influenza‌ A or Covid-19. In‌‌ this way, we aim for our work grounded‌ in verification to have‌ an impact on the‌‌ sciences, beyond engineering, which will feed back into‌ our core formal methods‌ community.

3 Research program‌‌

3.1 Automated and Interactive Theorem Proving

The VeriDis‌ team gathers experts in‌ techniques and tools for‌‌ automatic deduction and interactive theorem proving, and specialists‌ in methods and formalisms‌ designed for the development‌‌ of trustworthy concurrent and distributed systems and algorithms.‌ Our common objective is‌ twofold: first, we wish‌‌ to advance the state of the art in‌ automated and interactive theorem‌ proving, and their combinations.‌‌ Second, we work on making the resulting technology‌ available for the computer-aided‌ verification of distributed systems‌‌ and protocols. In particular, our techniques and tools‌ are intended to support‌ sound methods for the‌‌ development of trustworthy distributed systems that scale to‌ algorithms relevant for practical‌ applications.

VeriDis members from‌‌ Saarbrücken are developing the Spass 11workbench.‌ It currently consists of‌ one of the leading‌‌ automated theorem provers for first-order logic based on‌ the superposition calculus 40‌, a theory solver‌‌ for linear arithmetic 2, a CDCL2‌ based satisfiability solver and‌ a propositional converter to‌‌ clausal normal form. Recently, we developed a first-prototype‌ of a new generation‌ of solvers based on‌‌ SCL (Simple Clause Learning)48, 47,‌ 58.

VeriDis members‌ design effective quantifier elimination‌‌ methods and decision procedures for algebraic theories, supported‌ by their efficient implementation‌ in the Redlog5‌‌ and Logic1 systems.

An important objective of this‌ line of work is‌ the integration of theories‌‌ in automated deduction. Typical theories of interest, including‌ fragments of arithmetic, are‌ difficult or impossible to‌‌ express in first-order logic.‌ We therefore explore efficient, modular techniques for integrating‌ semantic and syntactic reasoning methods, develop novel combination‌ results and techniques for quantifier instantiation. These problems‌ are addressed from both sides, i.e. by embedding‌ decision procedures into the superposition framework or by‌ allowing an SMT solver to accept axiomatizations for‌ plug-in theories. We also develop specific decision procedures‌ for theories such as non-linear real arithmetic that‌ are important when reasoning about certain classes of‌ (e.g., real-time) systems but that also have interesting‌ applications beyond verification.

We rely on interactive theorem‌ provers for reasoning about specifications at a high‌ level of abstraction when fully automatic verification is‌ not (yet) feasible. An interactive proof platform should‌ help verification engineers lay out the proof structure‌ at a sufficiently high level of abstraction; powerful‌ automatic plug-ins should then discharge the resulting proof‌ steps. Members of VeriDis have ample experience in‌ the specification and subsequent machine-assisted, interactive verification of‌ algorithms. In particular, we contribute to the development‌ of methods and tools for verifying properties of‌ specifications written in the TLA+55 language,‌ partly supported by the TLA+ Foundation.‌ Our group in particular develops the TLA+‌ Proof System where proofs are expressed in a‌ declarative language and that calls upon several automatic‌ backends 4. Trust in the correctness of‌ the overall proof can be ensured when the‌ backends provide justifications that can be checked by‌ the trusted kernel of a proof assistant.

At‌ the intersection of automated and interactive theorem proving,‌ members of VeriDis formalize a framework in the‌ proof assistant Isabelle/HOL for representing the correctness and‌ completeness of automated theorem provers. This work encompasses‌ proof calculi such as ordered resolution or superposition,‌ as well as concrete prover architectures such as‌ Otter or DISCOUNT loops. It also covers the‌ most recent splitting techniques that bring proof calculi‌ closer to SMT solvers. Moreover, VeriDis members actively‌ collaborate with members of the Inria teams Mocqua‌ and Pesto, mobilizing theorem proving techniques and tools‌ to address verification and certification challenges from quantum‌ computing and cryptographic protocol verification.

3.2 Formal Methods‌ for Developing and Analyzing Algorithms and Systems

Theorem‌ provers are not used in isolation. We are‌ most interested in their support of sound methodologies‌ for modeling and verifying systems. In this respect,‌ members of VeriDis have gained expertise and recognition‌ in making contributions to formal methods for concurrent‌ and distributed algorithms and systems 3, 9‌, and in applying them to concrete use‌ cases. In particular, the concept of refinement38‌, 41, 59 in state-based modeling formalisms‌ is central to our approach because it allows‌ us to present a rational (re)construction of system‌ development. An important goal in designing such methods‌ is to establish precise proof obligations, many of‌ which can be discharged by automatic tools. This‌ requires taking into account specific characteristics of certain‌ classes of systems and tailoring the model to concrete computational models. Our‌ research in this area‌ is supported by carrying‌‌ out case studies for academic and industrial developments.‌ This activity benefits from‌ and influences the development‌‌ of our proof tools.

In this line of‌ work, we investigate specific‌ development and verification patterns‌‌ for particular classes of algorithms, in order to‌ reduce the work associated‌ with their verification. We‌‌ are also interested in applications of formal methods‌ and their associated tools‌ to the development of‌‌ systems that underlie specific certification requirements in the‌ sense of, e.g., Common‌ Criteria. Finally, we are‌‌ interested in the adaptation of model checking techniques‌ for verifying actual distributed‌ programs, rather than high-level‌‌ models.

Today, the formal verification of a new‌ algorithm is typically the‌ subject of a PhD‌‌ thesis, if it is addressed at all. This‌ situation is not sustainable:‌ algorithm developers and system‌‌ designers must be able to productively use verification‌ tools for validating their‌ algorithms and implementations. On‌‌ a high level, the goal of VeriDis is‌ to make formal verification‌ standard practice for the‌‌ development of distributed algorithms and systems, just as‌ symbolic model checking has‌ become commonplace in the‌‌ development of embedded systems and as security analysis‌ for cryptographic protocols is‌ becoming standard practice today.‌‌ Although the fundamental problems in distributed programming are‌ well-known, they pose new‌ challenges in the context‌‌ of modern system paradigms, including ad-hoc and overlay‌ networks or peer-to-peer systems,‌ and they must be‌‌ integrated for concrete applications.

Model checking.

The paradigm‌ of model checking is‌ based on automatically verifying‌‌ properties over a formal model of a system,‌ using mathematical foundations. Model‌ checking, while useful and‌‌ highly successful in practice, can encounter the infamous‌ state space explosion problem.‌ One direction of VeriDis‌‌ therefore addresses the efficiency of model checking, by‌ proposing new algorithms or‌ heuristics to speed up‌‌ analysis. We notably focus on the quantitative setting‌ (time, probabilities), and more‌ specifically on the parametric‌‌ paradigm where some quantitative constants are unknown, and‌ the goal becomes to‌ synthesize suitable valuations. A‌‌ recent application of the VeriDis team is that‌ of opacity (in the‌ more general field of‌‌ cybersecurity), addressed using model checking. The team considers‌ a novel definition of‌ opacity in timed automata,‌‌ where an attacker only has access to the‌ execution time; several recent‌ works address this direction.‌‌

Correctness by construction

Verification methods are used for‌ a wide variety of‌ algorithm classes. An alternative‌‌ to these verification methods involves design methods aimed‌ at producing algorithms or‌ programs that are correct‌‌ by construction. This approach is based on the‌ notion of refinement, and‌ we aim at identifying‌‌ fairly general patterns that guide the designer's steps.‌ In 37, we‌ contrast three techniques for‌‌ constructing correct algorithms by construction.

3.3 Verification and‌ Analysis of Dynamic Properties‌ of Biological Systems

The‌‌ unprecedented accumulation of information in biology and medicine‌ during the last 20‌ years led to a‌‌ situation where any new‌ progress in these fields is dependent on the‌ capacity to model and make sense of large‌ data. Until recently, foundational research was concerned with‌ simple models of 2 to 5 ordinary differential‌ equations. The analysis of even such simple models‌ was sufficiently involved that it resulted in one‌ or several scientific publications for a single model.‌ Much larger models are built today to represent‌ cell processes, explain and predict the origin and‌ evolution of complex diseases or the differences between‌ patients in precision and personalized medicine. For instance,‌ the biomodels.net model repository 56 contains thousands of‌ hand-built models of up to several hundreds of‌ variables. Numerical analysis of large models requires an‌ exhaustive scan of the parameter space or the‌ identification of the numerical parameters from data. Both‌ are infeasible for large biological systems because parameters‌ are largely unknown and because of the curse‌ of dimensionality: data, even rich, become rapidly sparse‌ when the dimensionality of the problem increases. On‌ these grounds, VeriDis researchers aim at formal symbolic‌ analysis instead of numerical simulation.

As an illustration‌ of the approach, consider BIOMD0000000716 in the above-mentioned‌ BioModels database, which models the transmission dynamics of‌ subtype H5N6 of the avian Influenza A virus‌ in the Philippines in August 2017 57.‌ This model describes four species (susceptible/infected bird or‌ human) together with their dynamics. Using purely symbolic‌ algorithms, we obtain a decomposition of the dynamics‌ into three subsystems ${T}_{1}$ , $T_{2‌}$ , and $T_{3}$ with attractive manifolds ${ℳ‌}_{1}$ , $ℳ_{2}$ and $ℳ_{3}$ .‌ The constant factors appearing in the corresponding differential‌ equations indicate that the system $T_{2}$ is‌ 125 times slower than $T_{1}$ , and‌ that $T_{3}$ is another 125 times slower.‌

Figure 1.b — Figure 1: Illustration‌ of the analysis of an epidemic model of‌ avian Influenza A.

This multiple time scale reduction‌ emphasizes a cascade of successive relaxations of model‌ variables. Figure 1(a) shows the surface of‌ $ℳ_{1}$ projected into 3D space, with the‌ line and the dot representing the submanifolds ${ℳ‌}_{2}$ and $ℳ_{3}$ . Figure 1(b)‌ illustrates the direction field of $T_{1}$ projected‌ into 2D space. The curve corresponds to ${ℳ‌}_{1}$ , indicating that the population of susceptible‌ birds relaxes and that these variables reach quasi-steady‌ state values. Figure 1(c) represents the direction‌ field of $T_{2}$ on $ℳ_{1}$ projected‌ into 2D space. The line corresponds to ${ℳ‌}_{2}$ , showing the relaxation of the population‌ of infected birds. Finally, figure 1(d) shows‌ the direction field of $T_{3}$ on ${ℳ‌}_{2}$ projected into 2D space. The dot corresponds‌ to $ℳ_{3}$ , indicating the relaxation of‌ the populations of susceptible and infected humans to‌ a stable steady state.

The computation time is less than a second.‌ The computation is based‌ on massive SMT solving‌‌ over various theories, including QF_LRA for tropicalizations, QF_NRA‌ for testing Hurwitz conditions‌ on eigenvalues, and QF_LIA‌‌ for finding sufficient differentiability conditions for hyperbolic attractivity‌ of critical manifolds. Gröbner‌ reduction techniques are used‌‌ for final algebraic simplification 54. Observe that‌ numerical simulation would not‌ be able to provide‌‌ such a global analysis of the overall system,‌ even in the absence‌ of symbolic parameters, as‌‌ is the case in our rather simple example.‌

4 Application domains

Distributed‌ algorithms and protocols are‌‌ found at all levels of computing infrastructure, from‌ many-core processors and systems‌ on chip to wide-area‌‌ networks. We are particularly interested in the verification‌ of algorithms that are‌ developed for supporting peer-to-peer‌‌ networks or cloud computing services. Computing infrastructure must‌ be highly available and‌ is ideally invisible to‌‌ the end user, therefore correctness is crucial. One‌ should note that standard‌ problems of distributed computing‌‌ such as consensus, group membership or leader election‌ have to be reformulated‌ for the dynamic context‌‌ of these modern systems. We are not ourselves‌ experts in the design‌ of distributed algorithms, but‌‌ we work together with domain experts on designing‌ formal models of these‌ protocols, and on verifying‌‌ their properties. These cooperations help us focus on‌ concrete algorithms and ensure‌ that our work is‌‌ relevant to the distributed algorithm community.

Our work‌ on symbolic procedures for‌ solving polynomial constraints finds‌‌ applications beyond verification. In particular, we have been‌ working in interdisciplinary projects‌ with researchers from mathematics,‌‌ computer science, systems biology, and system medicine on‌ the analysis of reaction‌ networks and epidemic models‌‌ in order to infer principal qualitative properties. Our‌ techniques complement numerical analysis‌ techniques and are validated‌‌ against collections of models from computational biology.

The‌ team uses extensions of‌ timed automata (such as‌‌ parametric timed automata 39) as an underlying‌ formalism to solve practical‌ questions. Our work on‌‌ parametric timed automata is partly motivated by applications‌ in cybersecurity. Foundational decidability‌ results and novel notions‌‌ of non-interference and opacity for this class of‌ automata allow us, for‌ example, to determine the‌‌ maximal frequency of attacker actions for the attack‌ to succeed (i.e., so‌ that these actions remain‌‌ invisible to the external observer). Our contributions give‌ rise to implementations in‌ the Imitator model checker.‌‌

5 Highlights of the year

Vincent Trélat received‌ the best paper award‌ at ABZ, the International‌‌ Conference on Rigorous State-Based Methods, for his paper‌ on safely encoding B‌ proof obligations in SMT-LIB‌‌26.

6 Latest software developments, platforms, open‌ data

6.1 Latest software‌ developments

6.1.1 SPASS Workbench‌‌

Name:
SPASS Automated Reasoning Workbench
Keywords:
Automated theorem‌ proving, Linear arithmetic solver,‌ Decision procedure
Functional Description:‌‌
The SPASS Workbench is a collection of tools‌ for various reasoning tasks‌ in logic. It currently‌‌ comprises the first-order theorem prover SPASS, a decision‌ procedure for linear (mixed)‌ arithmetic SPASS-IQ, a satisfiability‌‌ modulo theory (SMT) solver‌ for linear (mixed) arithmetic SPASS-SATT, a propositional satisfiability‌ (SAT) solver SPASS-SAT, a propositional conjunctive normal form‌ converter SPASS-CNF, and several prototypical implementations of SPASS-SCL.‌ The systems SPASS, SPASS-SAT and SPASS-CNF are accessible‌ via a web interface.
News of the Year:‌
We finished a first competition version of SPASS-SCL‌ and won the prize for the best newcomer‌ system at CASC-30. SPASS Workbench is developed at‌ the Max Planck Institute with contributions by Martin‌ Bromberger who now works in industry.
URL:
https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/‌
Publications:
hal-03531893, hal-03531889, hal-03531894
Contact:
Christoph‌ Weidenbach
Participants:
Lorenz Leutgeb, Martin Bromberger, Christoph Weidenbach‌

6.1.2 Goeland

Name:
Goeland
Keywords:
First-order logic, Automated‌ deduction, Automated Reasoning, Proof, Certification
Functional Description:
Goeland‌ is an automated theorem prover for first-order logic.‌ It relies on a concurrent tableaux-based proof-search procedure‌ that allows it to conduct a fair branch‌ exploration. The prover can perform deskolemization and produce‌ machine-checkable proofs in Rocq, LambdaPi and SC-TPTP. It‌ supports TPTP FOF and TFF files.
News of‌ the Year:
In 2025, the main new developments‌ were as follows:
- redesign of type system,
- support‌ for Rocq output,
- support for SC-TPTP output.
Johann‌ Rosain (ENS Lyon) contributes to the development and‌ maintenance of Goeland.
URL:
https://github.com/GoelandProver/Goeland
Publication:
tel-04526940
Contact:‌
Julie Cailler
Participants:
Julie Cailler, Johann Rosain

6.1.3‌ E-Cyclist

Keyword:
Cyclic proofs
Functional Description:
Checking the‌ soundness of cyclic induction reasoning for first-order logic‌ with inductive definitions (FOLID) is decidable but the‌ standard checking method is based on an exponential‌ complement operation for Büchi automata. We devised a‌ polynomial method “semi-deciding” this problem in a paper‌ presented at the CiSS2019 conference (Circularity in Syntax‌ and Semantics). E-Cyclist is an extension of the‌ Cyclist prover (http://www.cyclist-prover.org/) that integrates this method. It‌ successfully checked all the proofs included in the‌ Cyclist distribution. The implementation details have been presented‌ at SCSS 2021 (ID HAL: hal-02464242).
URL:
https://members.loria.fr/SStratulat/files/e-cyclist.zip‌
Contact:
Sorin Stratulat
Participant:
Sorin Stratulat

6.1.4 TLAPS‌

Name:
TLA+ proof system
Keyword:
Proof assistant
Functional‌ Description:
TLAPS is a platform for developing and‌ mechanically verifying proofs about specifications written in the‌ TLA+ language. The TLA+ proof language is hierarchical‌ and explicit, allowing a user to decompose the‌ overall proof into proof steps that can be‌ checked independently. TLAPS consists of a proof manager‌ that interprets the proof language and generates a‌ collection of proof obligations that are sent to‌ backend verifiers. The current backends include the tableau-based‌ prover Zenon for first-order logic, Isabelle/TLA+, an encoding‌ of TLA+ set theory as an object logic‌ in the logical framework Isabelle, an SMT backend‌ designed for use with any SMT-lib compatible solver,‌ and an interface to a decision procedure for‌ propositional temporal logic.
News of the Year:
In‌ 2025, the main new developments were:
- The integration‌ of TLAPS into the TLA+ Virtual Studio‌ Code Extension was consolidated.
- A solution for importing‌ the abstract syntax tree from the standard SANY‌ parser for TLA+ was explored, in view of replacing the bespoke‌ parser underlying TLAPS.
- The‌ standard library, as well‌‌ as the collection of examples, were consolidated and‌ extended.
- Various bug fixes.‌
URL:
https://tla.msr-inria.inria.fr/tlaps/content/Home.html
Contact:
Stephan‌‌ Merz
Participants:
Damien Doligez, Stephan Merz
Partner:
Microsoft‌

6.1.5 Logic1

Keywords:
First-order‌ logic, Quantifier Elimination, Computer‌‌ algebra system (CAS)
Scientific Description:

Logic1 offers a‌ robust framework for working‌ with first-order formulas. Its‌‌ implementations are designed to be generic and parameterized‌ by theories in the‌ sense of first-order logic,‌‌ currently supporting the theory of Sets and the‌ theory of Real Closed‌ Fields. Included algorithms cover‌‌ a range of tasks, such as computing normal‌ forms (CNF, DNF, NNF,‌ PNF), simplification, and quantifier‌‌ elimination.

Comprehensive documentation is available at docs.logic1.eu and‌ on GitHub.
Functional Description:‌

First-order logic recursively builds‌‌ terms from variables and a specified set of‌ function symbols with specified‌ arities, which includes constant‌‌ symbols with arity zero. Next, atomic formulas are‌ built from terms and‌ a specified set of‌‌ relation symbols with specified arities. Finally, first-order formulas‌ are recursively built from‌ atomic formulas and a‌‌ fixed set of logical operators.

Logic1 focuses on‌ interpreted first-order logic, where‌ the above-mentioned function and‌‌ relation symbols have implicit semantics, which is not‌ explicitly expressed via axioms‌ within the logical framework.‌‌ Typical applications include algebraic decision procedures and, more‌ generally, quantifier elimination procedures,‌ e.g., over the real‌‌ numbers.
News of the Year:

Version 0.2.0 of‌ Logic1 was released on‌ February 12, 2025, via‌‌ Conda-Forge. This release introduces a parallel implementation of‌ real quantifier elimination by‌ virtual substitution up to‌‌ degree two, based on the framework of Kosta‌ (2016). The framework permits‌ instantiation for higher degrees‌‌ through appropriate virtual substitution tables.

The simplifier extends‌ the standard Redlog simplifier‌ (Dolzmann–Sturm, 1995) by allowing‌‌ global substitution of implicit identities of the form‌ x = q and‌ x = q *‌‌ y, where x and y are variables and‌ q is a rational‌ number. In addition, Logic1‌‌ now supports rational polynomial coefficients rather than being‌ restricted to integer coefficients.‌

Finally, a programmatic interface‌‌ has been added to provide convenient access to‌ essential Redlog functionality via‌ process communication. This interface‌‌ includes several variants of real quantifier elimination and‌ simplification. In 2025, Logic1‌ exceeded 1,000 downloads.

Besides‌‌ members of VeriDis, Nicolas Faroß (Chalmers University) actively‌ contributes to the development‌ of Logic1.
URL:
https://github.com/logic1-eu/logic1‌‌
Contact:
Thomas Sturm
Participants:
Thomas Sturm, Nicolas Faroß,‌ Lorenz Leutgeb

6.1.6 Redlog‌

Name:
Reduce Logic System‌‌
Keywords:
Computer algebra system (CAS), First-order logic, Constraint‌ solving, Quantifier Elimination
Functional‌ Description:

Redlog is an‌‌ integral part of the interactive computer algebra system‌ Reduce. It supplements Reduce's‌ comprehensive collection of powerful‌‌ symbolic computation methods by supplying more than 100‌ functions on first-order formulas.‌

Redlog generally works with‌‌ interpreted first-order logic in contrast to free first-order‌ logic. Each first-order formula‌ in Redlog must exclusively‌‌ contain atoms from one particular Redlog-supported theory, which‌ corresponds to a choice‌ of admissible functions and‌‌ relations with fixed semantics.‌ Redlog-supported theories include Nonlinear Real Arithmetic (Real Closed‌ Fields), Presburger Arithmetic, Parametric QSAT (quantified satisfiability solving),‌ and many more.
News of the Year:
While‌ development efforts have primarily focused on the successor‌ system Logic1, Redlog remains available and is committed‌ to continued full support in the long term.‌ Historically, many authors from different institutions contributed to‌ the development of Redlog, the main maintainers have‌ been Thomas Sturm and Andreas Dolzmann (Schloss Dagstuhl).‌
URL:
https://www.redlog.eu/
Contact:
Thomas Sturm
Participants:
Thomas Sturm,‌ Andreas Dolzmann, Melanie Achatz, Marek Kosta, Aless Lasaruk,‌ Herbert Melenk, Winfried Neun, Andreas Seidl, Christoph Zengler,‌ Volker Weispfenning

6.2 New platforms

6.2.1 ODEbase

Participants:‌ Thomas Sturm.

Name:
Online Database of Biomodels‌ Involving Ordinary Differential Equations
Keywords:
Automated reasoning, Dynamical‌ systems, Interdisciplinary research, Qualitative analysis
Scientific Description:
Symbolic‌ Computation and Automated Reasoning allow qualitative answers to‌ biological questions. Qualitative methods analyze dynamical input systems‌ as formal objects, in contrast to investigating only‌ a subset of the state space, as is‌ the case with numerical simulation. A common format‌ used in mathematical modeling of biological processes is‌ the Systems Biology Markup Language SBML. However,‌ symbolic tools and libraries have a different set‌ of requirements for their input data than their‌ numerical counterparts. The use of SBML data in‌ Symbolic Computation and Automated Reasoning requires significant pre-processing‌ that combines automated translation steps with human interaction‌ and expertise. ODEbase provides pre-processed input data derived‌ from established existing biomodels.
Functional Description:
SBML, which‌ is technically an XML instance, has been designed‌ as a very liberal format, and contributors of‌ models are primarily researchers whose key expertise resides‌ in natural sciences. This creates a situation where‌ SBML features may be used in unexpected ways.‌ A sound presentation of corresponding models outside the‌ SMBL framework then requires expertise in the life‌ sciences as well as mathematical competence, primarily in‌ algebra and in dynamical systems. Technically we use‌ a set of Python tools, which we have‌ developed for the semi-automatic conversion of SBML models.‌ Since the conversion process is not fully automatic‌ and our resources are limited, we focus on‌ models that we identify as interesting for Symbolic‌ Computation and Automated Reasoning approaches. Our principal source‌ of models is the renowned online database biomodels.net‌.
News of the Year:
ODEbase has gained‌ further recognition and citations during 2025.
URL:
odebase.org‌
Publications:
hal-03651751
Contact:
Thomas Sturm
Partners:
Christoph Lüders‌ (University of Bonn, Germany), Ovidiu Radulescu (University of‌ Montpellier, France).

7 New results

7.1 Automated Deduction‌ Techniques

Graph Superposition for Quantum Circuits

Julie Cailler‌ , Florent Krasnopol , Sophie Tourret , joint‌ work with Noé Delormes and Simon Perdrix (project‌ team Mocqua).

Quantum circuits are studied by members‌ of the Mocqua team, as a means to‌ represent quantum computing algorithms. In this context, a‌ series of equations, called the coherence equations, define‌ an equivalence relation between circuits that represent the‌ same program. Being able to detect the equivalence of two circuits by‌ this relation is a‌ central problem in this‌‌ research domain.

The circuits can be naturally represented‌ using hypergraphs. We are‌ adapting a technique for‌‌ automated reasoning on graphs that uses the superposition‌ calculus to work on‌ circuits represented as a‌‌ particular class of graphs.

Challenging Benchmarks for Circuit‌ Equivalence Checks in SMT-LIB‌ and TPTP

Julie Cailler‌‌ , Sophie Tourret , joint work with Noé‌ Delormes (project team Mocqua).‌

Circuits, quantum or otherwise,‌‌ can be represented by first-order terms satifying a‌ given predicate ensuring that‌ some constraints that are‌‌ natural on the circuits are also true on‌ corresponding terms. By adding‌ constraints to the coherence‌‌ equations, it is also possible to represent them‌ as clauses in first-order‌ logic with arithmetic. We‌‌ have produced several encodings of this problem and‌ evaluated the performances of‌ the state-of-the-art automated theorem‌‌ provers (ATPs) Vampire and cvc5 on them. The‌ analysis of the results‌ suggests interesting directions of‌‌ further research for ATPs.

GNN for Word Equations‌ Solving

Julie Cailler joint‌ work with Parosh Aziz‌‌ Abdulla, Mohamed Faouzi Atig, Chencheng Liang (Univ. of‌ Uppsala, Sweden), Philipp Rümmer‌ (Univ. of Uppsala, Sweden‌‌ & Univ. of Regensburg, Germany).

Reasoning within theories‌ such as arithmetic, arrays,‌ and algebraic data structures‌‌ has become a key challenge in automated reasoning.‌ To address this, Satisfiability‌ Modulo Theories (SMT) solvers‌‌ have been developed, offering efficient decision procedures for‌ a wide range of‌ theories, including string theory.‌‌ Strings, as a fundamental data type in programming,‌ are crucial for many‌ domains like text processing,‌‌ database management, and web applications.

We developed a‌ new algorithm that leverages‌ a Graph Neural Network‌‌ (GNN)-guided approach for solving word equations, building upon‌ the well-known Nielsen transformation‌ for equation splitting. We‌‌ extend this algorithm to deal with conjunction of‌ word equations. To handle‌ the variable number of‌‌ conjuncts, three approaches to adapt a multi-classification task‌ to the problem of‌ ranking equations are proposed.‌‌ The training of the GNN is done with‌ the help of minimum‌ unsatisfiable subsets (MUSes) of‌‌ word equations.

The algorithm is implemented in a‌ solver named DragonLi. Experimental‌ results on both artificial‌‌ and real-world benchmarks demonstrate the efficiency of DragonLi‌ in solving satisfiable problems.‌ A paper presenting this‌‌ work was published at FroCoS 2025 14.‌

A Framework for Certifying‌ Tableaux Proofs in Rocq‌‌

Julie Cailler joint work with Johann Rosain (ENS‌ de Lyon).

The free-variable‌ tableau method has been‌‌ widely used in order to automate proofs in‌ multiple kinds of logics.‌ Many Automated Theorem Provers‌‌ (ATPs) still use this method, either because it‌ is the only one‌ available (e.g., in modal‌‌ logics) or in order to produce proofs. However,‌ as far as the‌ authors know, its results‌‌ have never been formalized. Together with Johann Rosain,‌ we develop TableauxRocq, a‌ deep-embedding of free-variable first-order‌‌ tableaux in the Rocq prover that uses the‌ Skolemization framework due to‌ Cantone and Nicolosi-Asmundo. This‌‌ tool can be used‌ as a certifier of ATPs by adapting the‌ Goéland prover to output proofs in the TableauxRocq‌ format, thus seeing a significant speed-up in the‌ checking time.

Non-Ground Congruence Closure

Hendrik Leidinger ,‌ Christoph Weidenbach .

Congruence closure on ground equations‌ is a well-established and efficient algorithm for deciding‌ ground equalities. It constructs an explicit representation of‌ ground equivalence classes based on a given set‌ of input equations, allowing ground equalities to be‌ decided by membership. In many applications, these ground‌ equations originate from grounding non-ground equations.

We propose‌ an algorithm that directly computes a non-ground representation‌ of ground congruence classes constructed from non-ground equations.‌ Our approach is sound and complete with respect‌ to the corresponding ground congruence classes. Experimental results‌ demonstrate that computing non-ground congruence classes often outperforms‌ the classical ground congruence closure algorithm in efficiency‌ 25.

Decision procedures for fragments with arithmetic.‌

Pascal Fontaine , joint work with Bernard Boigelot,‌ Thomas Braipson, Tom Clara, and Baptiste Vergain (Univ.‌ of Liège).

Arithmetic reasoning is an important aspect‌ of automated deduction applied to verification. Fragments mixing‌ arithmetic and uninterpreted symbols are often undecidable. We‌ study the decidability frontier of such fragments. In‌ particular, we are examining monadic first-order logic with‌ order interpreted over the real numbers. This fragment‌ is decidable, whereas adding the successor (or more‌ precisely the “

+​​﻿﻿ 1

”) function is‌ undecidable. Although this result has been known for‌ some time, no effective decision procedure exists. We‌ want to develop an effective procedure, first, because‌ a fundamental understanding of this fragment is scientifically‌ interesting, and second, because this deep understanding can‌ be inspirational for new SMT quantifier instantiation techniques‌ in the presence of arithmetic. We previously designed‌ and published one key element of this decision‌ procedure, namely the emptiness test of automata on‌ linear orderings 44. In 2025, we have‌ made progress towards the development of a quantifier‌ elimination method for automata on linear orderings.

The‌ SMT-LIB standard.

Pascal Fontaine , joint work with‌ Clark Barrett (Stanford University), Cesare Tinelli (University of‌ Iowa).

We are involved in the standardization of‌ the SMT-LIB language, a widely adopted format for‌ the input of SMT solvers. In 2025, we‌ released version 2.7 of the language, a transitional‌ version introducing maps (lambdas) and polymorphism. We are‌ currently working on version 3.0 which will be‌ based on higher-order logic, and will introduce a‌ flexible concept of modules, to replace the 2.x‌ concepts of theories and logic.

7.2 Interactive Theorem‌ Proving

Formalizing the Relationship Between SCL(FOL) and Ground‌ Ordered Resolution

Martin Bromberger , Martin Desharnais ,‌ Christoph Weidenbach .

Recently, it has been demonstrated‌ that simple clause learning for first-order logic SCL(FOL)‌ can simulate ground ordered resolution 49. We‌ revisit this result and provide a new formal‌ proof in Isabelle/HOL. The existing pen-and-paper proof is‌ monolithic and challenging to comprehend. In order to‌ improve clarity, we develop an alternative proof structured as eleven (bi)simulation steps‌ between the two calculi,‌ transitioning from ordered resolution‌‌ to SCL(FOL) 19. A key simulation lemma‌ ensures that, under certain‌ conditions, one simulation direction‌‌ can be automatically transferred to the other. Consequently,‌ for each of the‌ eleven steps, it suffices‌‌ to establish only one direction of simulation. The‌ complete proof is included‌ in the Isabelle Archive‌‌ of Formal Proofs.

An Extension of the‌ TPTP Derivation Format for‌ Sequent-Based Calculi.

Julie Cailler‌‌ , joint work with Simon Guilloud, Sankalp Gambhir,‌ Auguste Poiroux, Yann Herklotz,‌ Thomas Bourgeat, and Viktor‌‌ Kunčak (EPFL, Switzerland).

We introduce SC-TPTP, an extension‌ of the TPTP derivation‌ format for supporting proofs‌‌ expressed in the sequent formalism, enabling seamless proof‌ exchange between interactive theorem‌ provers and first-order automated‌‌ theorem provers. We provide a way to represent‌ non-deductive steps—Skolemization, clausification, and‌ Tseitin normal form—as deductive‌‌ steps within the format. Building upon the existing‌ support in the Lisa‌ proof assistant and the‌‌ Goéland theorem prover, the SC-TPTP ecosystem is further‌ enhanced with proof output‌ interfaces for Egg and‌‌ Prover9, as well as proof reconstruction support for‌ HOL Light, Lean, and‌ Rocq. A publication of‌‌ this work was accepted at CADE 24.‌

Integration of Abduction in‌ Isabelle/HOL.

Tiago Campos Ferreira‌‌ , Sophie Tourret , joint work with Haniel‌ Barbosa (Universidade Federal de‌ Minas Gerais, Brazil).

In‌‌ the context of the associate team Carma (cf.‌ Section 9), Sophie‌ Tourret and Haniel Barbosa‌‌ have started to work on a new collaborative‌ project. Tiago Campos Ferreira,‌ a master student under‌‌ Haniel Barbosa's supervision in Brazil, joined VeriDis in‌ October 2025 for an‌ internship of six months.‌‌ His objective is the integration of cvc5's abduction‌ mechanism into the proof‌ assistant Isabelle/HOL. Abduction is‌‌ a logical operation that provides tentative explanations to‌ statements in a given‌ theory. For a proof‌‌ assistant, it could be turned into a tool‌ that suggests missing hypotheses‌ or intermediary steps in‌‌ proofs. The SMT solver cvc5 is currently the‌ best tool for abduction‌ modulo theories, and Isabelle/HOL‌‌ is the proof assistant with the best automation.‌ By combining both into‌ a prototype tool, we‌‌ want to identify robustly the bottlenecks of abduction‌ and address them until‌ abduction becomes useful in‌‌ practice to help proof engineers.

Formalization of Modal‌ Model Theory in Isabelle/HOL‌

Sophie Tourret , joint‌‌ work with Jasmin Blanchette and Yiming Xu (LMU‌ Munich, Germany).

As a‌ well-established framework for talking‌‌ about relational structures, propositional modal logic has been‌ used and investigated for‌ decades 43. We‌‌ formalized the finite tree-like model property of multi-modal‌ logic in Isabelle/HOL, which‌ considers families of modal‌‌ operators. This property is valuable because a modal‌ logic is decidable if‌ it has the finite‌‌ model property and is finitely axiomatizable. To obtain‌ a general statement independent‌ of the type of‌‌ worlds constituting the universe of the semantics, we‌ used Isabelle/HOL's HOLZF extension‌ to prove the theorem.‌‌

Lean to DHOL Translation‌

Sophie Tourret , joint work with Jasmin Blanchette,‌ Alexander Bentkamp and Luca Maio (LMU Munich, Germany).‌

A new dependently-typed higher-order logic called DHOL has‌ recently been introduced 61 as a bridge between‌ existing dependently-typed logics, on which several major proof‌ assistants are based (e.g., Rocq, Lean), and classical‌ logics that benefit from strong automation. Whereas the‌ translation from DHOL to classical HOL was introduced‌ together with DHOL, the translation between DHOL and‌ other type theories remained to be established. We‌ define this translation and establish the appropriate theoretical‌ guarantees of soundness and completeness. A publication of‌ this work is in preparation.

Certification of Rewriting‌ on Circuits

Julie Cailler , Sophie Tourret ,‌ joint work with Noé Delormes and Simon Perdrix‌ (project team Mocqua).

Circuits as studied in the‌ Mocqua team are instances of signal flow graphs‌ that belong to the symmetric monoidal category known‌ as PROP. Circuits can also be interpreted as‌ directed hypergraphs with fixed inputs and outputs, but‌ this interpretation is not injective and thus builds‌ equivalence classes of circuits that correspond to the‌ same graph. This equivalence between circuits can be‌ defined by a set of equations called the‌ coherence equations. Thus, a straightforward proof that two‌ circuits are equivalent consists in a sequence of‌ atomic transformations, each justified by one application of‌ a coherence equation. We want to produce certificates‌ for these transformations that can be machine checked.‌ An obvious approach to handle this kind of‌ problems is to rely on terminating and confluent‌ term rewrite systems (TRSs), that can rewrite equivalent‌ terms to a unique normal form. However, there‌ is no such TRS that can handle the‌ coherence equations. We devised a technique to produce‌ certificates by decomposing the problem into two subproblems,‌ that of state-and-effect-free PRO (the fragment of PROP‌ where wires cannot cross each other, corresponding to‌ isoplanar graphs), and that of trivial PROPs (corresponding‌ to permutations of wires) that we have proved‌ to both possess terminating and confluent TRSs. We‌ are working at producing these certificates in Isabelle/HOL,‌ using its simplifier as the term-rewriting engine to‌ normalize terms. We have achieved a proof-of-concept implementation‌ for state-and-effect-free PROs, and are now working on‌ the same for trivial PROPs, before we finally‌ consider full PROPs.

Reconstruction of SMT Proofs in‌ Lambdapi.

Alessio Coltellacci , Stephan Merz , joint‌ work with Bruno Andreotti and Haniel Barbosa (Universidade‌ Federal de Minas Gerais, Brazil) and with Frédéric‌ Blanqui (project team Deducteam).

SMT solvers are widely‌ considered as the tools of choice for the‌ automatic verification of programs and systems. Their integration‌ with skeptical proof assistants requires proofs found by‌ SMT solvers to be certified by the trusted‌ kernel of proof assistants. The Alethe format 62‌ represents a trace of an SMT proof, explaining‌ why a set of SMT constraints is unsatisfiable.‌ In this work, we aim at interpreting Alethe‌ proof traces and generating corresponding proofs that are accepted by the Lambdapi‌ proof checker, a foundational‌ proof assistant based on‌‌ dependent type theory and rewriting rules that is‌ intended to serve as‌ a pivot for exchanging‌‌ proofs between interactive proof assistants. Whereas elementary Alethe‌ rules can directly be‌ mirrored by corresponding proof‌‌ rules derived in Lambdapi, some rules describe an‌ algorithm for checking an‌ assertion. This is true‌‌ in particular for rules about

n

-ary connectives,‌ as well as for‌ checking theorems in linear‌‌ (integer or real) arithmetic. In these cases, we‌ leverage the technique of‌ proof by reflection by‌‌ setting up a semi-decision procedure on a suitable‌ data type.

A first‌ paper covering the pure‌‌ logic fragment of SMT-LIB was accepted for publication‌ in the journal Acta‌ Informatica (to appear in‌‌ 2026), a second paper focusing on the reconstruction‌ of proofs in linear‌ arithmetic was presented at‌‌ FroCoS 2025 20. A comprehensive description of‌ the approach appears in‌ the PhD thesis of‌‌ Alessio Coltellacci, to be defended in January 2026.‌

An Isabelle/HOL framework to‌ Add Splitting on Top‌‌ of Saturation Calculi

Ghilain Bergeron , Florent Krasnopol‌ , Sophie Tourret .‌

Saturation-based calculi, such as‌‌ resolution and superposition, are implemented in theorem provers‌ to establish the satisfiability‌ of sets of formulas‌‌ in various logics. In some circumstances, such calculi‌ introduce needless dependencies in‌ their steps. Splitting is‌‌ a technique that removes such dependencies by introducing‌ branching between independent pieces‌ of formulas. It is‌‌ very successful and has been adopted in various‌ forms by most state-of-the-art‌ provers. We have formalized‌‌ in Isabelle/HOL the splitting framework 52 that models‌ several forms of splitting‌ in a modular way.‌‌ The formalization focuses on a first model of‌ splitting and an instance‌ of resolution extended with‌‌ splitting called Lightweight AVATAR. The results of this‌ work were presented at‌ ITP 2025 17.‌‌

Towards the Verification of ProVerif in Isabelle/HOL

Qi‌ Qiu , Sophie Tourret‌ , joint work with‌‌ Steve Kremer (project team Pesto).

ProVerif is a‌ cryptographic protocol verifier developed‌ by project team Prosecco‌‌ with real-world applications (including TLS or the Signal‌ messaging protocol). The Inria‌ team Pesto uses ProVerif‌‌ and made several contributions to the tool. At‌ its heart, ProVerif is‌ built upon the well-known‌‌ resolution calculus applied to Horn clauses, and the‌ tailoring to security protocols‌ lies in the encoding‌‌ of protocols as logic formulas rather than in‌ the reasoning. We have‌ started a direct formalization‌‌ in Isabelle/HOL of the core technique in ProVerif,‌ leveraging our previous work‌ on the formalization of‌‌ saturation-based calculi including resolution 63.

Analysing the‌ Divergence of Induction-based Proofs.‌

Sorin Stratulat .

Primal‌‌ grammars have been used recently to detect divergence‌ in induction-based and automatically-generated‌ proofs 46. A‌‌ divergence is detected if, from a fixed number‌

n

(

> 2﻿﻿﻿‌

) of generated conjectures,‌‌ one can build a Presburger system that can‌ subsume further conjectures which‌ are no longer processed.‌‌ We have shown that‌ the Presburger systems built in that way can‌ also subsume false conjectures, for any

n

,‌ which limits drastically the use of primal grammars‌ in sound induction-based inference systems.

A Verified Encoding‌ of Proof Obligations.

Vincent Trélat , Ghilain Bergeron‌ , Stephan Merz , Sophie Tourret .

The‌ B and Event-B methods for formal system development‌ are widely used for developing certified embedded systems,‌ for example in the railway domain. These methods‌ identify a significant number of proof obligations that‌ must be discharged in order for a system‌ development to be acceptable for certification authorities. Since‌ a high degree of proof automation is essential‌ in an industrial context, proofs are routinely delegated‌ to automatic theorem provers, including SMT solvers. In‌ a recent experiment conducted by the Clearsy company,‌ among the roughly 77,000 proof obligations of a‌ representative development project, 64% were proved automatically by‌ the Atelier B tool suite, leaving 28,000 obligations‌ to be proved by human interaction. The existing‌ encoding of B proof obligations for SMT solvers‌ 50 systematically reduces formulas to first-order logic, eliminating‌ all constructs of set theory. A drawback of‌ this approach is that it destroys the structure‌ of formulas, in particular for constructs such as‌ set comprehension that involve binders. In this work,‌ we develop an alternative encoding that takes advantage‌ of recent capabilities of SMT solvers to handle‌ fragments of higher-order logic.

An encoding in SMT-LIB,‌ the input language of SMT solvers, of proof‌ obligations based on these ideas has been implemented‌ in the Lean proof assistant, and an evaluation‌ on the fragment of the benchmark mentioned above‌ that is covered by the encoding indicates that‌ this translation is a useful complement to the‌ existing first-order encoding: the solvers succeed in proving‌ a high number of obligations that they failed‌ to prove for the previous encoding. A paper‌ describing this work 26 was presented at ABZ‌ 2025 and received the best paper award.

By‌ developing the encoding in Lean, it becomes possible‌ to establish its correctness within that proof assistant.‌ To this end, the semantics of B and‌ SMT formulas have been formalized in Lean, and‌ work is in progress in order to formally‌ prove the correctness of the translation.

Moreover, a‌ tool has been developed for representing proof obligations‌ corresponding to formal developments in B directly in‌ Lean, with a particular emphasis on identifying well-definedness‌ conditions arising from possibly undefined expressions, such as‌ the minimum value of a set or the‌ application of a partial function. A paper describing‌ this work is in preparation for submission to‌ an international conference.

7.3 Formal Methods for Developing‌ and Analyzing Algorithms and Systems

Formalization and Implementation‌ of Safe Destination Passing in Pure Functional Programming‌ Settings.

Thomas Bagrel , Horatiu Cirstea , joint‌ work with Arnaud Spiwack (Tweag & Modus Create).‌

Destination-passing style programming introduces destinations, which represent the‌ address of a write-once memory cell. These destinations can be passed as‌ function parameters, allowing the‌ caller to control memory‌‌ management: the callee simply fills the cell instead‌ of allocating space for‌ a return value. While‌‌ typically used in systems programming, destination passing also‌ has applications in pure‌ functional programming, where it‌‌ enables programs that were previously not expressible using‌ ordinary immutable data structures.‌

We developed a core‌‌ $λ$ -calculus with destinations 15. This new‌ calculus is more expressive‌ than similar existing systems,‌‌ with destination passing designed to be as flexible‌ as possible. This is‌ achieved through a modal‌‌ type system combining linear types with a system‌ of ages to manage‌ scopes, in order to‌‌ make destination-passing safe. Type safety of our core‌ calculus was proved formally‌ with the Rocq proof‌‌ assistant.

Then, we see how this core calculus‌ can be adapted to‌ an existing pure functional‌‌ language, Haskell, whose type system is less powerful‌ than our custom theoretical‌ one 32. Retaining‌‌ safety comes at the cost of removing some‌ flexibility in the handling‌ of destinations. We later‌‌ refine the implementation to recover much of this‌ flexibility, at the cost‌ of increased user complexity.‌‌ The prototype implementation in Haskell shows encouraging results‌ for adopting destination-passing style‌ programming when traversing or‌‌ mapping over large data structures such as lists‌ or data trees. A‌ comprehensive presentation of these‌‌ results appears in Thomas Bagrel's PhD thesis 32‌.

Verified Code Generation‌ from PlusCal Programs.

Ghilain‌‌ Bergeron , Horatiu Cirstea , Stephan Merz .‌

Specifications written in high-level‌ languages such as TLA‌‌+ are useful for verifying correctness properties. They‌ often result in state‌ spaces that remain manageable‌‌ for model checking, and they allow users to‌ design inductive invariants that‌ are at the heart‌‌ of deductive system verification. However, there is a‌ substantial gap between high-level‌ specifications of algorithms and‌‌ implementations of those algorithms in actual programs. One‌ way to avoid this‌ gap is to translate‌‌ specifications into code in a programming language that‌ can be compiled and‌ executed. In this work,‌‌ we investigate the feasibility of such an approach‌ for algorithms written in‌ Distributed PlusCal, an algorithmic‌‌ language that can be translated to TLA+‌ for verification. We define‌ a series of PlusCal‌‌ fragments together with semantics-preserving translations from one fragment‌ to the next one,‌ and then aim at‌‌ implementing a code generator for the most restrictive‌ fragment.

A translator from‌ a suitable fragment of‌‌ Distributed PlusCal to the Go language has been‌ implemented in Lean based‌ on this approach, and‌‌ the correctness of the first two phases of‌ the translation has been‌ proved. This work was‌‌ presented at WPTE 2025 27, and we‌ have been invited to‌ prepare an extended paper‌‌ for an international journal. Work on formal proofs‌ of the correctness of‌ the translation in the‌‌ Lean proof assistant is ongoing.

Gröbner Bases for‌ Boolean Function Minimization.

Simon‌ Schwarz , joint work‌‌ with Nikolas Faroß (Chalmers‌ University).

Boolean function minimization techniques try to find,‌ for a given formula, a smaller equivalent formula.‌ We present a novel technique for heuristic multi-level‌ Boolean function minimization. By using an algebraic encoding,‌ we embed the minimization problem into an algebraic‌ domain, where algorithms for computing Gröbner bases become‌ applicable. A Gröbner basis usually forms a compact‌ representation of our encoded function. From the Gröbner‌ basis, we then reconstruct an equivalent, more compact‌ Boolean formula. The minimized formula is in the‌ language of Boolean formulas with negation, conjunction, disjunction‌ and exclusive-or operations. To the best of our‌ knowledge, our approach is the first to use‌ Gröbner bases for function minimization. We evaluate our‌ approach on Boolean formulas created from arithmetic operations‌ as well as on random formulas. Compared to‌ state-of-the-art exact minimization algorithms, our approach can handle‌ formulas with up to three times as many‌ variables. Empirically, we obtain very compact formulas. In‌ particular, our algorithm is especially efficient if there‌ exists a comparatively small equivalent formula or if‌ the minimized formula contains exclusive-or operations. In practice,‌ such functions occur, e.g., in embedded systems or‌ cryptography. Overall, our approach forms a new, interesting‌ trade-off between result minimality and runtime 13.‌

Formalization and verification of a train scheduler in‌ TLA+.

Martin Vassor , Lucas Villaume‌ , joint work with Guillaume Bonfante (Carbone Team‌ of LORIA).

In the context of Cyber Humanum‌ Est 45, Guillaume Bonfante created a small‌ scale train model. Trains run on routes automatically,‌ following traffic lights. A scheduler is in charge‌ of controlling railroad switches and traffic lights, thus‌ indirectly controlling trains. The model is a simplified‌ version of rules used in real train networks.‌

In order to prevent crashes (two trains colliding)‌ or deadlocks (two trains being locked, e.g. facing‌ each other), one has to ensure that the‌ scheduler never allows such situations to occur. Therefore,‌ we formalized the traffic rules in TLA+‌, allowing to model check the correctness of‌ a schedule. In a second step, we show‌ how schedules can be composed while remaining correct,‌ allowing one to manage large train networks.

Reversibility‌ for Fault Tolerance in Typed Sessions.

Martin Vassor‌ , joint work with Adam Barwell (University of‌ St. Andrews, Scotland), Ping Hou (University of Oxford,‌ England), and Nobuko Yoshida (University of Oxford, England).‌

Multiparty Session Types (MPST) are a family of‌ type-based techniques developed to prevent various classes of‌ bugs in message-passing concurrent programs, such as the‌ absence of deadlock. MPST are also used as‌ a form of protocol specification, where the well-typedness‌ of a program ensures its conformance to the‌ specification (session fidelity). However, MPST often assume a‌ reliable model of communication, i.e. without message loss‌ or process faults, and existing approaches to relax‌ this assumption either augment MPST with additional elements‌ to deal with faults (e.g. placing explicit checkpoints‌ in the protocol specification), or lower the guarantees provided (e.g. Affine MPST,‌ which safely stops the‌ whole system in case‌‌ of a process failure, losing session fidelity).

In‌ this project, we aim‌ to implement MPST on‌‌ top of a reversible variant of the higher-order‌ $π$ -calculus. In such‌ a setting, upon the‌‌ failure of a process, we expect the system‌ to transparently revert to‌ a previous state, thus‌‌ recovering from the failure. Contrary to existing approaches‌ based on reversibility, we‌ do not modify the‌‌ syntax or the semantics of MPST, allowing users‌ to transparently switch from‌ standard MPST to fault-tolerant‌‌ MPST.

A paper describing this work was published‌ at the International Conference‌ on Reversible Computing 16‌‌.

Bounded Reversibility in HO $π$

Martin Vassor‌ , joint work with‌ Ivan Lanese (University of‌‌ Bologna and Inria - Université Côte d'Azur, Italy),‌ and Claudio A. Mezzina‌ (University of Urbino, Italy).‌‌

Reversible process calculi are variants of process calculi‌ such as CCS or‌

π

-calculus, which are‌‌ equipped with forward and backward semantics. Forward semantics‌ correspond to the usual‌ ones of those process‌‌ calculi, while backward semantics allows for actions to‌ be undone (e.g., undoing‌ a message reception). When‌‌ designing such calculi, the community often aims at‌ complete and causally-consistent backward‌ semantics, where causal consistency‌‌ means that states reached using backward reduction rules‌ ought to be reachable‌ from the initial state‌‌ using only forward rules (i.e., reverting does not‌ allow new states to‌ be reached), and completeness‌‌ means that any such state ought to be‌ reachable.

While those two‌ key properties are desirable,‌‌ as they lead to nice theoretical frameworks, they‌ are not suitable for‌ practical use. Indeed, completeness‌‌ entails that enough information has to be kept‌ during execution to reach‌ the initial state. Causal‌‌ consistency entails that reverting part of the system‌ possibly spreads to all‌ components. Those two consequences‌‌ are problematic in practice: the first one due‌ to the amount of‌ information that has to‌‌ be kept forever, even if it is not‌ used in the end.‌ In the second one,‌‌ the spread of rollback disallows standard software architectures‌ such as client-server, in‌ which one would not‌‌ allow the rollback of a client to spread‌ to the server, and‌ then to other clients.‌‌

29 contains preliminary work addressing those issues. We‌ drafted a reversible higher-order‌ $π$ calculus with additional‌‌ primitives for committing messages, preventing them to be‌ rolled back in the‌ rest of the computation‌‌ (thus breaking completeness, but allowing the garbage-collection of‌ rollback information). We also‌ introduce non-causally-consistent uses of‌‌ communication channels, in which case the rollback spread‌ is not propagated through‌ such uses (thus breaking‌‌ causal consistency, but allowing some spatial control of‌ rollbacks).

An inductive invariant‌ for a high-level Raft‌‌ specification

Volkan Burakcin , Stephan Merz .

Raft‌ 60 is a protocol‌ for achieving iterated consensus‌‌ that is used in the implementation of many‌ distributed systems. Although the‌ original author of Raft‌‌ accompanied the design by‌ a TLA+ specification, it is written at‌ a very low level of abstraction and is‌ therefore hard to verify using model checking or‌ theorem proving. We have been working on a‌ more high-level specification of the protocol that makes‌ it easier to understand the main mechanisms underlying‌ Raft. During the internship of Volkan Burakcin ,‌ an inductive invariant for Raft was designed and‌ proved correct using TLAPS, the TLA+ Proof‌ System, cf. Section 6.1.4. The invariant implies‌ the main correctness properties of Raft, in particular‌ the existence of a single leader for any‌ given term, the agreement of two entries at‌ the same index provided the terms of the‌ entries are identical, the fact that any leader‌ contains all committed entries, and the property that‌ committed entries are stable.

7.4 Algorithmic Verification

Degradation‌ of stochastic systems

Baptiste Diedler , Marie Duflot-Kremer‌ , Engel Lefaucheux , Bastien Pichet .

Diagnosis‌ aims at providing information about specific unobservable behaviors‌ of a system, such as failures. The study‌ of diagnosis in stochastic systems, such as those‌ based on Markov chains, is now well-developed. For‌ instance, in 42, the authors demonstrate, for‌ various forms of diagnosis, how to determine whether‌ a system is diagnosable and, if so, how‌ to construct a diagnoser, i.e., a tool that‌ translates a sequence of observations into a verdict.‌

During the internships of Baptiste Diedler and Bastien‌ Pichet, we extended this classical framework by introducing‌ the notion of degradation. Degradation generalizes diagnosis by‌ aiming not only to detect whether a fault‌ has occurred, but also to quantify the amount‌ of damage suffered by the system. In this‌ setting, failures may accumulate over time, and the‌ objective becomes to detect when the accumulated degradation‌ exceeds a given threshold. This work is ongoing,‌ with the goal of submitting a paper next‌ year.

Multi-agent transfer systems

Engel Lefaucheux , joint‌ work with Nathalie Bertrand, Loïc Helouet and Luca‌ Paparazzo (project team Devine).

In 35, we‌ introduced multi-agent transfer systems, a cooperative model in‌ which agents move on individual weighted arenas while‌ managing non-negative energy levels and sharing energy with‌ peers. Each agent has a target vertex, and‌ the goal is to reach a global configuration‌ where all targets are achieved simultaneously. We considered‌ different execution semantics (namely asynchronous, strongly synchronous, and‌ weakly synchronous), depending on whether the agents need‌ to act simultaneously or not. Such a game‌ under either the asynchronous and strongly synchronous semantics‌ can be turned into a Petri net. However,‌ the weakly synchronous semantic produces a model that‌ is strictly more expressive than Petri nets.

We‌ investigated the computational complexity of the resulting global‌ reachability problem. For asynchronous and strongly synchronous semantics,‌ we established decidability and derived complexity bounds ranging‌ from NP to EXPSPACE, relying on monotonicity and‌ bounded witness arguments. In contrast, we showed that‌ reachability becomes undecidable under weakly synchronous semantics due to the loss of‌ monotonicity.

7.5 Foundational Research‌ in Arithmetic Reasoning

On‌‌ the number of real types of univariate polynomials.‌

Thomas Sturm , joint‌ work with Thomas Faroß‌‌ (Chalmers University).

We consider univariate polynomials with real‌ coefficients. The real type‌ of a family

{f﻿‌​‌}_{1}

, ...,

{f﻿​​﻿}_{n}

of such polynomials‌ is their combined sign‌ behavior from

- ∞﻿‌​‌

\infty

, presented as column vectors of‌ length

n

. For‌ instance, all real roots‌‌ of

f_{1} =﻿​​﻿ x + 1

,‌

f_{2} = 2﻿﻿﻿‌ x + 1

,‌‌

f_{3} = {x﻿​​﻿}^{2} - 1

are‌ located at

- 1﻿﻿﻿‌

- \frac{1}{2﻿‌​‌}

, 1. Evaluation of the signs of

{[​​​‌ f_{1}, {f﻿﻿﻿‌}_{2}, f_{3﻿‌​‌}]}^{T}

at and between those points yields‌ the real type

\begin{matrix} [﻿﻿﻿‌ r] - 1﻿‌​‌ & 0 & 1 & 1 & 1﻿​​﻿ & 1 & 1​​​‌ \\ - 1 & - 1﻿﻿﻿‌ & - 1 & 0 & 1﻿‌​‌ & 1 & 1 \\ 1 & 0﻿​​﻿ & - 1 & - 1​​​‌ & - 1 & 0 & 1﻿﻿﻿‌ \end{matrix} .

We are specifically‌‌ interested in the number of possible real types‌ of families of $n‌$ polynomials subject to a‌‌ degree bound $d$ . Košta 53 has given‌ a formula for the‌ number $R_{d}$ of‌‌ possible real types of a single polynomial of‌ degree $d$ in terms‌ of summations of certain‌‌ binomial coefficients, and conjectured that this number could‌ not be expressed in‌ a closed form. We‌‌ are not aware of any former results for‌ $n > 1$ .‌

Considering finite families ${f‌‌}_{1}$ , ..., ${f}_{n}$ of polynomials of‌ degrees $d_{1}$ ,‌ ..., $d_{n}$ ,‌‌ and denoting by $m$ the finite cardinality of‌ the union of their‌ real roots, we have‌‌ derived the following results:

In the special case‌ $n = 1$ ,‌ we simplify Košta's result‌‌ mentioned above to a simple case distinction based‌ on Fibonacci numbers, which‌ can be expressed in‌‌ closed form, in contrast to sums of binomial‌ coefficients.
On these grounds,‌ we derived another closed‌‌ form for the number ${\hat{R}}_{d}$ of‌ all real types realized‌ by a single polynomial‌‌ up to degree $d$ . It follows that‌ both $R_{d}$ ,‌ ${\hat{R}}_{d} \in‌‌ Θ (φ^{d})$ , where $φ‌$ is the golden ratio,‌ and $Θ$ is the‌‌ Bachmann–Landau symbol for asymptotic growth of the same‌ order.
For the general‌ case $n \geq 1‌‌$ , we derive a formula for the number‌ $R_{d_{1},‌ \dots, d_{n‌‌}}^{(m)}$ of all real types realized‌ by polynomials with degrees‌ $d_{i}$ and $m‌‌$ distinct real roots. Summation over $m$ yields an‌ explicit form for the‌ number $R_{d_{1‌‌}, \dots, {d}_{n}}$ of all real‌ types realized by polynomials‌ with degrees $d_{i‌‌}$ and any number of roots, which generalizes Košta's‌ original result.
For the‌ number of all real‌‌ types realized by polynomials‌ with any choice of $d_{1}$ , ...,‌ $d_{n}$ and $m$ distinct real roots, we‌ can reduce or formula for $R_{d_{1‌}, \dots, {d}_{n}}$ to the closed‌ form $S_{n}^{( m)} = {2‌}^{n} \cdot {({3}^{n} - 1)‌}^{m}$ , which generalizes the obvious $S_{1‌}^{(m)} = 2^{m + 1‌}$ . In particular, this imposes an upper bound‌ on $R_{d_{1}, \dots, {d‌}_{n}}^{(m)}$ .

Real types for‌ $n > 1$ play a key role in‌ a number of decision and quantifier elimination procedures‌ for real closed fields. Our results were published‌ at ISSAC 23.

8 Bilateral contracts and‌ grants with industry

8.1 Bilateral contracts with industry‌

Participants: Thomas Bagrel, Horatiu Cirstea, Marie‌ Duflot-Kremer, Engel Lefaucheux, Dominique Méry,‌ Stephan Merz, Mohamed Amine Snoussi.

Type‌ systems for the memory safety of functional programs‌

Duration:
April 2022 – March 2025
Industrial Partner:‌
Tweag
Team participants:
Thomas Bagrel , Horatiu Cirstea‌
Summary:
In his PhD thesis 32 supported by‌ a CIFRE contract, Thomas Bagrel studies type systems‌ and corresponding constructions in a pure functional calculus‌ with destinations at its core for guaranteeing programs‌ that are memory safe and can be compiled‌ to efficient machine code.

Reengineering protocols for industrial‌ controllers

Duration:
May 2023 – April 2026
Industrial‌ Partner:
Westinghouse France
Team participants:
Mohamed Amine Snoussi‌ , Marie Duflot-Kremer , Engel Lefaucheux , Stephan‌ Merz
Summary:
In his PhD work supported by‌ a CIFRE contract, Amine Snoussi aims at constructing‌ formal models and simulations of protocols that are‌ used for industrial controllers, in particular for the‌ diagnosis and control of electronic components in nuclear‌ power plants. He has modeled the main protocol‌ for the interaction between a controller and a‌ component as a system of timed automata and‌ verified a number of properties using the UppAal‌ model checker. He also developed a simulator of‌ the protocol that can interact with an actual‌ controller.

Event-B modeling for Human-Machine Interaction

Duration:
June‌ 2024 – June 2025
Industrial Partner:
SAS H-AUGENPLUS‌
Team participants:
Dominique Méry
Summary:
The objective of‌ this work is to assist in the development‌ of Event-B models for HMI systems.

9 Partnerships‌ and cooperations

9.1 International initiatives

9.1.1 Associate Teams‌ in the framework of an Inria International Lab‌ or in the framework of an Inria International‌ Program

Title:
CAtalyzing progRess in smt solving and‌ proof assistants via Modularity, proof trAnslation, and proof‌ reconstruction (CARMA)
Duration:
2024 - 2026
Coordinators:
Sophie‌ Tourret and Haniel Barbosa (UFMG)
Partners:
Universidad Federal‌ de Minas Gerais, Belo Horizonte (Brazil)
Inria contact:‌
Sophie Tourret
Team participants:
Tiago Campos Ferreira ,‌ Alessio Coltellacci , Stephan Merz , Sophie Tourret‌ , Vincent Trélat
Summary:

The Carma associate team‌ aims at improving the state of the art‌ in SMT solving on three fronts. Our first objective is to design‌ a new SMT solver‌ as a research vessel‌‌ that emphasizes modularity over utmost performance. Our goal‌ is that all components‌ can simply be plugged‌‌ in and out to make it easy to‌ upgrade and serve as‌ a platform for comparison‌‌ between different techniques. The tentative name of this‌ new solver is ModulariT.‌ Our second objective concerns‌‌ higher-order SMT and the missing components to make‌ it competitive. We plan‌ to provide an efficient‌‌ conflict-based instantiation technique for higher-order logic for ModulariT.‌ Our third objective concerns‌ the coexistence of various‌‌ proof formats for SMT solving. We aim at‌ more interoperability so that‌ the various formats do‌‌ not create a divide in the community. Specifically,‌ our aim will be‌ to provide a translation‌‌ of Alethe proofs generated by SMT solvers to‌ Dedukti, a logical framework‌ based on the $λ‌‌ Π$ -calculus modulo, that has become the lingua‌ franca of proof translation.‌ In 2024, we added‌‌ a fourth objective to the team, that of‌ studying the integration of‌ SMT-based abduction in a‌‌ proof assistant.

In 2025, there were again several‌ exchanges between Belo Horizonte‌ and Nancy, despite cancellations‌‌ of trips in the spring related to the‌ late vote of the‌ budget in France. A‌‌ master student from Belo Horizonte, Tiago Campos Ferreira‌ is visiting us for‌ a 4 months master‌‌ internship funded by Orion, a program within the‌ excellence initiative of Lorraine‌ University. He is working‌‌ on our fourth objective with Sophie Tourret and‌ Haniel Barbosa. A PhD‌ student from our team‌‌ (Alessio Coltellacci ) and a postdoc from‌ Deducteam (part of the‌ associate team) visited Belo‌‌ Horizonte for 3 weeks to work on our‌ first objective. Some more‌ trips have been anticipated‌‌ for early 2026 to counteract the previously mentioned‌ delays.

9.1.2 Participation in‌ other International Programs

Title:‌‌
Artificial Intelligence based Robotics (AiRobo)
Partner Institution(s):
- University‌ of Macedonia, Greece
- RWTH,‌ Germany
- Eszterhazy Karoly Catholic‌‌ University, Hungary
- West University of Timisoara, Romania
Date/Duration:‌
December 2023 - November‌ 2026
Team participant:
Sorin‌‌ Stratulat
Summary:
AiRobo 51 is an ERASMUS+ project‌ that aims to increase‌ the quality and the‌‌ attractivity of related departments at the partner universities,‌ by a significant raise‌ of the level of‌‌ competence and skills of the relevant academic staff‌ in the field of‌ Artificial Intelligence based Robotics.‌‌ The correct functioning of such safety-critical systems is‌ ensured by formal verifications‌ using theorem provers such‌‌ as Theorema and Coq, as well as SAT‌ and SMT solvers such‌ as SMT-RAT.

9.2 National‌‌ initiatives

ANR Project BiSoUS

Title:
Better Synthesis for‌ Underspecified Quantitative Systems
Duration:‌
March 2023 – February‌‌ 2027
Coordinator:
Didier Lime, École Centrale de Nantes‌ & LS2N
Partner Institutions:‌
- IRISA, Rennes
- LIPN, University‌‌ Sorbonne Paris Nord (Paris 13)
- LS2N École Centrale‌ de Nantes (coordinator)
- LMF,‌ University Paris-Saclay
Team participants:‌‌
Marie Duflot-Kremer , Engel Lefaucheux
Summary:
Computer systems‌ are ubiquitous and identifying‌ their possible defects is‌‌ crucial already at the‌ earliest stages of their development, when many aspects,‌ including the environments or the execution platforms, have‌ not been fixed. Verification must then be performed‌ on underspecified models and should give understandable answers.‌ In this project, we aim at developing verification‌ techniques for underspecified models that take this explainability‌ constraint into account, by optimizing resources, such as‌ energy or memory, and synthesizing more precise requirements‌ on the underspecified aspects of the models under‌ which the system behaves correctly. We depart from‌ classical formalisms and consider their combined extensions with‌ three complementary ingredients: costs/rewards for resource consumption; parameters‌ for unknown quantitative characteristics; and games for representing‌ all the behaviours of the underspecified system.
Keywords:‌
Verification, Model checking, parametrised systems, games with guarantees‌
More information:
BiSoUS Web site

ANR Project BLaSST‌

Title:
Enhancing B Language Reasoners Using SAT and‌ SMT Techniques
Duration:
March 2022 – February 2027‌
Coordinator:
Stephan Merz
Partner Institutions:
- Inria Nancy (coordinator)‌
- University of Artois & CRIL, Lens
- CLEARSY, Aix-en-Provence‌
- University of Liège, Belgium
Team participants:
Pascal Fontaine‌ , Stephan Merz , Vincent Trélat , Sophie‌ Tourret
Summary:
The BLaSST project targets bridging combinatorial‌ and symbolic techniques in automatic theorem proving, in‌ particular for proof obligations generated from B models.‌ It focuses on advancing the state of the‌ art in automated reasoning, in particular SAT and‌ SMT techniques, and on making these techniques available‌ to software verification. More specifically, encoding techniques, optimized‌ resolution techniques, model generation, and lemma suggestion will‌ be investigated. The expected scientific impact is a‌ substantially higher degree of automation of solvers for‌ expressive input languages by leveraging higher-order reasoning and‌ enumerative instantiations over finite domains, as well as‌ useful feedback for verification conditions that cannot be‌ proved. The effectiveness of the techniques developed in‌ the project will be quantified by applying them‌ to benchmark sets provided by the industrial partner.‌ The industrial impact of BLaSST will be a‌ higher productivity of proof engineers. The collections of‌ benchmarks and the reasoning engines will be made‌ openly available under permissive open-source licenses.
Keywords:
B‌ method, deductive verification, SAT, SMT, higher-order logic
More‌ information:
BLaSST Web site

ANR Project EBRP

Title:‌
Enhancing EventB and RODIN: EventB-Rodin-Plus
Duration:
January 2020‌ – December 2026
Coordinator:
Dominique Méry
Partner Institutions:‌
- INPT-ENSEEIHT & IRIT, Toulouse
- CentraleSupelec & LRI
- University‌ of Lorraine & LORIA
- University Paris-Est Créteil &‌ LACL
- University of Düsseldorf, Germany
- University of Southampton,‌ School of Electronics and Computer Science, United Kingdom‌
Team participants:
Dominique Méry
Keywords:
formal IDE, theory,‌ proof management, cyber-physical systems, discrete models, continuous models,‌ refinement, verification, tools
Summary:
The purpose of EBRP‌ is to enhance Event-B and the corresponding Rodin‌ toolset. This will be done by engaging in‌ some basic research dealing with various mathematical theories‌ that are not currently available in Event-B and‌ Rodin. The development of complex systems usually involves‌ different scientific disciplines and skills. For instance, modeling‌ behaviors and interactions of autonomous systems may require concepts from control theory‌ such as differential equations,‌ communication protocols, resource allocation,‌‌ access control rules, etc. EBRP targets the definition‌ of extension mechanisms for‌ Event-B rather than defining‌‌ domain-specific modeling languages, and implementing those mechanisms within‌ Rodin.
More information:
EBRP‌ Web site

ANR Project‌‌ ICSPA

Title:
Interoperable and Confident Set-based Proof Assistants‌
Duration:
January 2022 –‌ December 2026
Coordinator:
Catherine‌‌ Dubois, ENSIIE & Samovar
Partner Institutions:
- ENSIIE &‌ Samovar, Évry
- Inria (Nancy‌ and Saclay research centers)‌‌
- University Paul Sabatier & IRIT, Toulouse
- University of‌ Montpellier & LIRMM, Montpellier‌
- CLEARSY, Aix-en-Provence
Team participants:‌‌
Alessio Coltellacci , Dominique Méry , Stephan Merz‌
Summary:
The B, Event-B,‌ and TLA+ formal‌‌ methods are based on different flavors of set‌ theory. The ICSPA project‌ aims at formally relating‌‌ these different theories for allowing users (i) to‌ independently certify proofs carried‌ out using the automatic‌‌ proof tools developed for these formal methods and‌ (ii) to transfer developments,‌ including their proofs, carried‌‌ out in one of these languages to another‌ one. The objectives are‌ to reinforce confidence in‌‌ developments carried out using these methods and to‌ enable interoperability between them.‌ The foundation for achieving‌‌ these goals lies in the encoding of the‌ set theories in the‌ Dedukti logical framework developed‌‌ at Inria Saclay, which implements the $λ Π‌$ -calculus modulo.
Keywords:
B‌ method, TLA+,‌‌ set theory, logical framework
More information:
ICSPA Web‌ site

10 Dissemination

10.1‌ Promoting scientific activities

Julie‌‌ Cailler :
- Editor of the Newsletter of the‌ Association of Automated Reasoning‌ (AAR).

10.1.1 Scientific events:‌‌ organization

General chair, scientific chair

Julie Cailler :‌ Artifact Evaluation co-chair of‌ SPIN 2025 (Hamilton, Canada)‌‌
Stephan Merz :
- PC co-chair and co-organizer of‌ the TLA+ Community‌ Meeting 2025 (Hamilton, Canada)‌‌
- PC co-chair and co-organizer of the 12th Workshop‌ on Formal Reasoning on‌ Distributed Algorithms (Berlin, Germany)‌‌
Sophie Tourret :
- PC co-chair of the SMT‌ workshop 2025 (Glasgow, UK)‌
- PC co-chair and co-organizer‌‌ of the workshop Weidenbach60 (Stuttgart, Germany).
Uwe Waldmann‌ :
- PC co-chair of‌ CADE 2025 (Stuttgart, Germany),‌‌
- PC co-chair of Deduktionstreffen 2025 (Stuttgart, Germany).
Christoph‌ Weidenbach : PC co-chair‌ of FroCos 2025 (Reykjavik,‌‌ Iceland).

Member of organizing committees

Julie Cailler :‌
- LVP days 2025, Strasbourg,‌ France.
Marie Duflot-Kremer :‌‌
- Journées sciences et médias (together with journalists and‌ other scientific associations) 2025,‌ Paris, France.
Pascal Fontaine‌‌ :
- Organizing committee of the summer school VTSA‌ 2025 in Liège, Belgium.‌
Stephan Merz :
- Organizing‌‌ committee of the summer school VTSA 2025 in‌ Liège, Belgium.
Sophie Tourret‌ :
- workshop chair of‌‌ CADE 2025 (Stuttgart, Germany),
- co-organizer of the “reflection”‌ seminar, a joint project‌ with Institut Élie Cartan‌‌ de Lorraine and the Poincaré archives, that will‌ take place as a‌ series in Nancy in‌‌ 2026,
- co-organizer of the “deduction” seminar series for‌ its next two iterations‌ at Dagstuhl, Germany. One‌‌ is already accepted and scheduled for early 2026.‌
Christoph Weidenbach :
- Organizing‌ committee of the summer‌‌ school VTSA 2025 in‌ Liège, Belgium.

10.1.2 Scientific events: selection

Member of‌ conference program committees

Julie Cailler : TASE 2025,‌ FMCAD Student Forum 2025, FSTTCS 2025 (artifact PC‌ committees: VMCAI 2025).
Horatiu Cirstea : RuleML 2025.‌
Engel Lefaucheux : QEST-FORMATS 2025.
Dominique Méry :‌ iFM2025, ABZ2025, TASE2025, ICFEM2025.
Stephan Merz : ABZ‌ 2025, CADE 2025, FMICS 2025, VECOS 2025.
Thomas‌ Sturm : CASC 2025, SYMCOMP 2025 (and workshop:‌ SC-Square 2025).
Sophie Tourret : CADE 2025, ITP‌ 2025 (and workshops: SMT 2025, Weidenbach60).
Uwe Waldmann‌ : KI 2025.
Christoph Weidenbach : CADE 2025.‌

10.1.3 Journals

Editor in Chief

Thomas Sturm :‌ Mathematics in Computer Science, Springer.

Member of the‌ editorial boards

Thomas Sturm : Journal of Symbolic‌ Computation, Elsevier.
Christoph Weidenbach : Journal of Automated‌ Reasoning, Springer.

Reviewer - reviewing activities

Julie Cailler‌ : Journal of Applied Logic, Journal of Logical‌ and Algebraic Methods in Programming, Science of Computer‌ Programming.
Horatiu Cirstea : book chapter for ISTE‌ Press.
Stephan Merz : Formal Methods in System‌ Design, Software Tools for Technology Transfer (2 articles).‌
Sophie Tourret : Journal of Artificial Intelligence Research,‌ Transactions on Computational Logic, Automated Reasoning, Logical Methods‌ in Computer Science.
Uwe Waldmann : Journal of‌ Symbolic Computation.

10.1.4 Invited talks

Julie Cailler :‌
- Deskolemization: From Tableaux to Proof Certificates, CHoCoLa Meeting,‌ Lyon, France
- Goéland: A Concurrent Tableau-Based ATP that‌ Produces Machine-Checkable Proofs, EuroProofNet School on Natural Formal‌ Mathematics, University of Bonn, Germany
Stephan Merz :‌ The TLA+ Framework – From High-Level Specifications‌ to Distributed Programs, 20th Intl. Conf. Integrated Formal‌ Methods, Paris, France.
Christoph Weidenbach : Cars,‌ Wine, Logic & more. Weidenbach60, Stuttgart, Germany.‌

10.1.5 Leadership within the scientific community

Julie Cailler‌ :
- Co-chairperson of the LVP (Langages et‌ Vérification de Programmes) group of GDR GPL.‌
Stephan Merz :
- chair of the TLA+‌ Specification Language Committee,
- member of the Governing Board‌ of the TLA+ Foundation,
- member of IFIP‌ WG 2.2 (Formal Specification of Programming Concepts).
Thomas‌ Sturm :
- advisory positions in the EPRSC Projects‌ EP/T015748/1 and EP/T015713/1, UK,
- SC-Square steering committee member,‌ invited in 2023.
Sophie Tourret :
- CADE trustee,‌ elected in 2022, reelected in 2025,
- PAAR workshop‌ steering committee member, invited in 2020,
- Ex-officio SMT‌ trustee for 2025,
- SAT/SMT/AR coordination committee member, invited‌ in 2024.
Uwe Waldmann :
- CADE trustee, ex-officio‌ in 2024, elected in 2025,
- co-speaker of GI‌ FG Deduktionssysteme.
Christoph Weidenbach :
- president of AAR,‌
- FroCos steering committee member.

10.1.6 Scientific expertise

Stephan‌ Merz : assessment of a promotion request at‌ the University of Delaware, U.S.A.
Sophie Tourret :‌ reviewer for a project submitted to the Israel‌ Science Foundation.

10.1.7 Research administration

Horatiu Cirstea :‌
- member of the hiring committee for an associate‌ professor position at Toulouse INP - ENSEEIHT /‌ IRIT.
Stephan Merz :
- coach for ERC project‌ applications at Inria,
- scientific referent for European affairs‌ (project REIL) at University of Lorraine,
- member of‌ the bureau du comité des projets at Inria Nancy,
- chairman of the‌ hiring committee for an‌ associate professor position at‌‌ IDMC, University of Lorraine.
Sophie Tourret :
- EuroProofNet‌ European COST action core‌ member, deputy leader of‌‌ working group 2 on automated theorem provers,
- member‌ of the doctoral commission‌ of Inria centre at‌‌ University of Lorraine,
- member of the hiring committee‌ for an associate professor‌ position at Polytech Paris-Saclay,‌‌
- member of the Bill McCune PhD Award committee.‌
Uwe Waldmann :
- member‌ of MPG CIS W2‌‌ tenure track selection committees 2024/2025 and 2025/2026,
- ombudsperson‌ of MPI-INF.

10.2 Teaching‌ - Supervision - Juries‌‌ - Educational and pedagogical outreach

10.2.1 Teaching

The‌ university employees of VeriDis‌ have a statutory teaching‌‌ obligation of 192 hours per year. We only‌ list the teaching activities‌ at the master level.‌‌

Master: Julie Cailler , Software engineering, 20 HETD,‌ 2A (M1), ENSEM, France.‌
Master: Horatiu Cirstea ,‌‌ Programming paradigms, 32 HETD, M2 Informatique, Université de‌ Lorraine, France.
Master: Horatiu‌ Cirstea , Software analysis‌‌ and design, 80 HETD, M1 informatique, Université de‌ Lorraine, France.
Master: Horatiu‌ Cirstea , Software engineering,‌‌ 50 HETD, 2A (M1), ENSEM, Université de Lorraine,‌ France.
Master: Marie Duflot-Kremer‌ , Using unplugged activities‌‌ to pass on computer science concepts to students,‌ 35 HETD, master for‌ future teachers, Université de‌‌ Lorraine, France
Master: Marie Duflot-Kremer , Elements of‌ model checking, 16 HETD,‌ M2 Informatique, Université de‌‌ Lorraine, France.
Master: Marie Duflot-Kremer , Distributed algorithms,‌ 15 HETD, M1 Informatique,‌ Université de Lorraine, France.‌‌
Master: Marie Duflot-Kremer and Engel Lefaucheux, supervision of‌ 3 students in a‌ short initiation à la‌‌ recherche internship, M1, Université de Lorraine
Master: Dominique‌ Méry , Formal Modeling‌ for Software-based Systems 40‌‌ HETD, M2 Informatique, Université de Lorraine, France.
Master:‌ Dominique Méry , Models‌ and algorithms, M1 Telecom‌‌ Nancy, 48 HETD, Université de Lorraine, France.
Master:‌ Dominique Méry , Formal‌ Modeling for Software-based Systems,‌‌ M2 Telecom Nancy, 24 HETD, Université de Lorraine,‌ France.
Master: Stephan Merz‌ , Elements of model‌‌ checking, 16 HETD, M2 Informatique, Université de Lorraine,‌ France.
Master: Stephan Merz‌ , Distributed algorithms, 15‌‌ HETD, M1 Informatique, Université de Lorraine, France.
Master:‌ Stephan Merz , Secure‌ Coding, M1 Mines Nancy,‌‌ 13 HETD, Université de Lorraine, France.
Master: Thomas‌ Sturm , Decision Procedures‌ for Specific Theories (Seminar),‌‌ Universität des Saarlandes, Germany.
Master: Sophie Tourret ,‌ Secure Coding, M1 Mines‌ Nancy, 13 HETD, Université‌‌ de Lorraine, France.
Master: Martin Vassor , Distributed‌ Algorithms, 16HETD, 4th years,‌ Polytech Nancy, Université de‌‌ Lorraine, France.
Master: Martin Vassor , Foundation of‌ Cybersecurity, 24.5HETD, 2A, Mines‌ Nancy, Université de Lorraine,‌‌ France.
Master: Martin Vassor , Python for engineers,‌ 40.5 HETD, 2A and‌ 3A, Mines Nancy, Université‌‌ de Lorraine, France.
Master: Uwe Waldmann , Automated‌ Reasoning, 60 HETD, Universität‌ des Saarlandes, Germany.
Master:‌‌ Christoph Weidenbach , Competitive Programming, 60 HETD, Universität‌ des Saarlandes, Germany.
Master:‌ Christoph Weidenbach , Automated‌‌ Reasoning, 60 HETD, Universität des Saarlandes, Germany.
Master:‌ Christoph Weidenbach , Decision‌ Procedures for Specific Theories‌‌ (Seminar), Universität des Saarlandes,‌ Germany.

10.2.2 Supervision

PhD completed: Thomas Bagrel ,‌ Formalization and Implementation of Safe Destination Passing in‌ Functional Programming Languages 32. University of Lorraine.‌ Supervised by Horatiu Cirstea , since April 2022,‌ defended in November 2025.
PhD completed: Martin Desharnais‌ , Verification in Isabelle/HOL of automated reasoning results‌ 33, MPI for Informatics, Saarland University. Supervised‌ by Jasmin Blanchette, Martin Bromberger , Sophie Tourret‌ and Christoph Weidenbach , since August 2021, defended‌ in January 2025.
PhD completed: Hendrik Leidinger ,‌ SCL(EQ): Simple Clause Learning in First-Order Logic with‌ Equality 34. Supervised by Christoph Weidenbach ,‌ defended in June 2025.
PhD in progress: Ghilain‌ Bergeron , Generating distributed programs from formal specifications.‌ University of Lorraine. Supervised by Horatiu Cirstea and‌ Stephan Merz , since October 2023.
PhD in‌ progress: Yasmine Briefs , A Unifiying Reasoning Framework‌ for SAT, SMT and First-Order Logic. Supervised by‌ Christoph Weidenbach , since April 2025.
PhD in‌ progress: Alessio Coltellacci , Reconstructing SMT Proofs in‌ Lambdapi. Supervised by Stephan Merz , since January‌ 2023.
PhD in progress: Sarah Dépernet , Model-checking‌ security properties on Timed automata. Supervised by Engel‌ Lefaucheux and Stephan Merz , since September 2024.‌
PhD in progress: Florent Krasnopol , Automated Theorem‌ Proving over the Reals for Reasoning on Quantum‌ Circuits. Supervised by Julie Cailler , Sophie Tourret‌ , and Stephan Merz , since September 2025.‌
PhD in progress: Lorenz Leutgeb , Automated Reasoning‌ about Constraint Horn Clauses. Supervised by Christoph Weidenbach‌ , since October 2022.
PhD in progress: Simon‌ Schwarz , Automatic Reasoning for Security. Supervised by‌ Thomas Sturm and Christoph Weidenbach , since October‌ 2022.
PhD in progress: Mohamed Amine Snoussi ,‌ Reengineering of an Industrial Communication Protocol. Supervised by‌ Marie Duflot-Kremer , Engel Lefaucheux , and Stephan‌ Merz , since May 2023.
PhD in progress:‌ Vincent Trélat , Higher-Order SMT Solving for Proof‌ Obligations in Set Theory. University of Lorraine. Supervised‌ by Stephan Merz and Sophie Tourret , since‌ October 2023.
Master completed: Yasmine Briefs , Formalizing‌ CDCL(T). Supervised by Christoph Weidenbach , March 2025.‌
Bachelor completed: Christian Michel , SCL(FOL) with Propositional‌ Abstraction. Supervised by Christoph Weidenbach , February 2025.‌
Master internship in progress: Tiago Campos Ferreira ,‌ Integrating SMT-based abduction in the proof assistant Isabelle/HOL,‌ since October 2025. Supervised by Sophie Tourret .‌
Master internship: Lucas Villaume , Formalisation and verification‌ of a train scheduler in TLA+,‌ Spring semester 2025. Supervised by Martin Vassor .‌
Bachelor internship: Volkan Burakcin , Correctness proof of‌ Raft, Spring semester 2025. Supervised by Stephan Merz‌ .
Bachelor internship: Baptiste Diedler , Degradation of‌ stochastic systems, Spring semester 2025. Supervised by Marie‌ Duflot-Kremer and Engel Lefaucheux .
Bachelor internship: Bastien‌ Pichet , Degradation of stochastic systems, Spring semester‌ 2025. Supervised by Marie Duflot-Kremer and Engel Lefaucheux‌ .

10.2.3 Juries

Julie Cailler was a member‌ of the jury for the French national high‌ school teacher competitive exam in computer science (CAPES NSI).
Marie Duflot-Kremer was‌ a member of the‌ board (secrétaire générale) of‌‌ the jury for the French national high school‌ teacher competitive exam in‌ computer science (CAPES NSI).‌‌
Stephan Merz was a reviewer and member of‌ the PhD committees of‌ theses at IPP Paris,‌‌ University of Saclay, and University of Strasbourg.

10.2.4‌ Educational and pedagogical outreach‌

Julie Cailler , Marie‌‌ Duflot-Kremer , and Sophie Tourret gave a talk‌ and a lab session‌ on formal verification for‌‌ a training program for teachers in France (PNF),‌ Nancy.
Marie Duflot-Kremer gave‌
- two talks and activities‌‌ on unplugged computer science for a training program‌ for teachers in France‌ (PNF), online,
- one workshop‌‌ at a séminaire de pédagogie universitaire on including‌ unplugged activities in a‌ computer science curriculum, Université‌‌ de Lorraine, Nancy.
- a talk about popularization activities‌ at the annual day‌ of LIP6 lab, Paris.‌‌
- a talk about popularization activities at the new‌ staff Inria seminar, Strasbourg.‌
Stephan Merz gave a‌‌ lecture (6 hours) on Specifying and Verifying Algorithms‌ in TLA+ at‌ the VTSA summer school‌‌ in Liège, Belgium.
Sophie Tourret gave
- a lecture‌ at the SAT/SMT/AR summer‌ school 2025 (St Andrews,‌‌ Scotland), and
- a talk at the CP/SAT Doctoral‌ Program 2025 (Glasgow, Scotland).‌

10.3 Popularization

10.3.1 Specific‌‌ official responsibilities in science outreach structures

Julie Cailler‌ and Marie Duflot-Kremer co-organized‌ Le stage des cigognes‌‌, a one week experience of research in‌ maths and computer science‌ for high school girls.‌‌
Marie Duflot-Kremer is the deputy vice-president for outreach‌ activities in the supervisory‌ council of SIF (‌‌Société Informatique de France).
Thomas Sturm was‌ involved in the organization‌ of the scientific training‌‌ of the German team for the International Olympiad‌ in Informatics (IOI).
Christoph‌ Weidenbach is the head‌‌ of the steering committee of the German Computer‌ Science Competition for High‌ School Students (BWINF) and‌‌ a co-organizer and the president of the jury‌ of the final round,‌ which took place in‌‌ Munich in September 2025. Thomas Sturm was a‌ member of that jury.‌

10.3.2 Participation in Live‌‌ events

Marie Duflot-Kremer :
- Journée décodeuses du numérique‌, unplugged activities workshop,‌ organized by CNRS, Paris,‌‌
- Journées filles et sciences, unplugged activities workshop‌ for secondary school girls,‌ lycée Loritz, Nancy,
- Mathematics‌‌ week, presentation of outreach unplugged activities for teachers,‌ rectorat de Nancy,
- one‌ day of training secondary‌‌ school students and two live shows of informagic‌ for 300 and 400‌ students, lycée Vauban, Luxembourg,‌‌
- Journées du matrimoine, explaining research in formal‌ verification, Jarville,
- a popularization‌ tour with 12 workshops‌‌ ranging from kindergarden to secondary school audience over‌ 4 days, Montereau-Fault-Yonne,
- a‌ talk for general audience‌‌ on unplugged activities, Montereau-Fault-Yonne,
- Journée d'initiative citoyenne en‌ faveur de l'égalité femmes-hommes‌, a short talk‌‌ on women in science, Vandœuvre-lès-Nancy,
- two days of‌ fête de la science‌, training and supervising‌‌ first year students realizing unplugged computer science workshops‌ for a general audience,‌ Université de Lorraine, Vandœuvre-lès-Nancy,‌‌

10.3.3 Other activities related‌ to science outreach

Julie Cailler :
- Chiche: 1‌ scientifique, 1 classe
- MATh.en.JEANS
Marie Duflot-Kremer :
- Chiche:‌ 1 scientifique, 1 classe, 4 talks to‌ secondary school students, Fameck,
- referent researcher of a‌ group of secondary school kids doing research for‌ the Math.en.JEANS program.

11 Scientific production

11.1 Major‌ publications

1 inproceedingsT.Thomas Bouton, D.‌ C.Diego Caminha B. de Oliveira, D.‌David Déharbe and P.Pascal Fontaine. veriT:‌ an open, trustable and efficient SMT-solver.Proc.‌ Conference on Automated Deduction (CADE)5663Lecture Notes‌ in Computer ScienceMontreal, CanadaSpringer2009,‌ 151-156
2 articleM.Martin Bromberger, T.‌Thomas Sturm and C.Christoph Weidenbach. A‌ complete and terminating approach to linear integer solving‌.Journal of Symbolic Computation100September 2020‌, 102-136HAL DOIback to text
3‌ incollectionD.Dominique Cansell and D.Dominique Méry‌. The Event-B Modelling Method - Concepts and‌ Case Studies.Logics of Specification LanguagesMonographs‌ in Theoretical Computer ScienceSpringerFebruary 2008,‌ 33-140HAL back to text
4 inproceedingsD.‌Denis Cousineau, D.Damien Doligez, L.‌Leslie Lamport, S.Stephan Merz, D.‌Daniel Ricketts and H.Hernán Vanzetto. TLA+‌ Proofs.18th International Symposium On Formal Methods‌ - FM 20127436Lecture Notes in Computer‌ ScienceParis, FranceSpringer2012, 147-154back‌ to text
5 articleA.Andreas Dolzmann and‌ T.Thomas Sturm. Redlog: Computer algebra meets‌ computer logic.ACM SIGSAM Bull.312‌1997, 2-9back to text
6 article‌H.Hassan Errami, M.Markus Eiswirth,‌ D.Dima Grigoriev, W. M.Werner M‌ Seiler, T.Thomas Sturm and A.Andreas‌ Weber. Detection of Hopf bifurcations in chemical‌ reaction networks using convex coordinates.Journal of‌ Computational Physics291March 2015, 279 -‌ 302HAL DOI
7 bookF.Fred Kröger‌ and S.Stephan Merz. Temporal Logic and‌ State Systems.Texts in Theoretical Computer Science‌Springer2008, 436URL: http://hal.inria.fr/inria-00274806/en/
8 article‌E.Evgeny Kruglov and C.Christoph Weidenbach.‌ Superposition Decides the First-Order Logic Fragment Over Ground‌ Theories.Mathematics in Computer Science64‌2012, 427-456
9 incollectionS.Stephan Merz‌. The Specification Language TLA+.Logics of‌ specification languagesMonographs in Theoretical Computer ScienceSpringer‌2008, 401-452HALback to text
10‌ inproceedingsT.Thomas Sturm and A.Ashish Tiwari‌. Verification and synthesis using real quantifier elimination‌.Proc. ISSAC 2011San Jose, United States‌ACM PressJune 2011, 329HAL DOI‌
11 inproceedingsC.Christoph Weidenbach, D.Dilyana‌ Dimova, A.Arnaud Fietzke, M.Martin‌ Suda and P.Patrick Wischnewski. SPASS Version‌ 3.5.22nd International Conference on Automated Deduction‌ (CADE-22)5663LNAIMontreal, CanadaSpringer2009,‌ 140-145back to text

11.2 Publications of the‌ year

International journals

12 articleR.Rosalie Defourné. Encoding TLA+ proof‌ obligations safely for SMT‌.Science of Computer‌‌ Programming239103178January 2025HAL DOI
13‌ articleN.Nicolas Faroß‌ and S.Simon Schwarz‌‌. Gröbner Bases for Boolean Function Minimization.‌Mathematics in Computer Science‌1912025,‌‌ 7HAL DOI back to text

International peer-reviewed‌ conferences

14 inproceedingsP.‌ A.Parosh Aziz Abdulla‌‌, M. F.Mohamed Faouzi Atig, J.‌Julie Cailler, C.‌Chencheng Liang and P.‌‌Philipp Rümmer. When GNNs Met a Word‌ Equations Solver: Learning to‌ Rank Equations.FroCoS‌‌ 202515979Lecture Notes in Computer ScienceReykavik,‌ IcelandSpringer Nature Switzerland‌September 2025, 327-345‌‌HAL DOI back to text
15 inproceedingsT.‌Thomas Bagrel and A.‌Arnaud Spiwack. Destination‌‌ Calculus: A Linear λ-Calculus for Purely Functional Memory‌ Writes.Proceedings of‌ the ACM on Programming‌‌ Languages, Volume 9, Issue OOPSLA1Article No.: 89, Pages‌ 253 - 279OOPSLA‌ 2025 - ACM Conference‌‌ on Object Oriented Programming Systems Languages and Applications‌9OOPSLA1Singapore, Singapore‌ACMApril 2025,‌‌ 253-279HAL DOI back to text
16 inproceedings‌A.Adam Barwell,‌ P.Ping Hou,‌‌ M.Martin Vassor and N.Nobuko Yoshida.‌ Encoding Choice and Replication‌ in roll-π.International‌‌ Conference on Reversible ComputationInternational Conference on Reversible‌ Computation15716Lecture Notes‌ in Computer ScienceOdense‌‌ (Danemark), DenmarkJune 2025, 27-36HAL DOI‌back to text
17‌ inproceedingsG.Ghilain Bergeron‌‌, F.Florent Krasnopol and S.Sophie Tourret‌. Formalizing Splitting in‌ Isabelle/HOL.ITP 2025‌‌ - 16th International Conference on Interactive Theorem Proving‌Reykjavik, IcelandSchloss Dagstuhl‌ – Leibniz-Zentrum für Informatik‌‌2025HAL DOI back to text
18 inproceedings‌N.Nathalie Bertrand,‌ L.Loïc Hélouët,‌‌ E.Engel Lefaucheux and L.Luca Paparazzo.‌ Reachability in multi-agent transfer‌ systems.VMCAI 2026‌‌ - 27th International Conference on Verification, Model Checking,‌ and Abstract InterpretationLNCS‌Rennes, France2026HAL‌‌
19 inproceedingsM.Martin Bromberger, M.Martin‌ Desharnais and C.Christoph‌ Weidenbach. A Stepwise‌‌ Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution‌.Automated Deduction –‌ CADE 30: 30th International‌‌ Conference on Automated Deduction, Stuttgart, Germany, July 28-31,‌ 2025, Proceedings15943Stuttgart,‌ GermanyJuly 2025HAL‌‌back to text
20 inproceedingsA.Alessio Coltellacci‌ and S.Stephan Merz‌. Checking Linear Integer‌‌ Arithmetic Proofs in Lambdapi.FroCoS 2025 -‌ 15th International Symposium Frontiers‌ of Combining Systems15979‌‌Lecture Notes in Computer ScienceReykjavik, IcelandSpringer‌ Nature Switzerland2025,‌ 367-385HAL DOI back‌‌ to text
21 inproceedingsI.I Dramnesc,‌ E.E Abraham,‌ N.N Fachantidis,‌‌ T.T Jebelean, G.G Kusper and‌ S.Sorin Stratulat.‌ AIROBO: A EUROPEAN PROJECT‌‌ FOR SOFTWARE ENGINEERS.EDULEARN 2025 - 17th‌ International Conference on Education‌ and New Learning Technologies‌‌EDULEARN25 ProceedingsPalma De Majorque, SpainJune 2025‌, 1221-1228HAL DOI‌
22 inproceedingsI.Isabela‌‌ Dramnesc, E.Erika‌ Abraham, N.Nikolaos Fachantidis, T.Tudor‌ Jebelean, G.Gabor Kusper and S.Sorin‌ Stratulat. AiRobo: A EU Project on Artificial‌ Intelligence and Robotics for Higher Education.ED-MEDIA‌ 2025 - EdMedia + Innovate LearningED-MEDIA 2025‌ - EdMedia + Innovate LearningBarcelona, SpainMay‌ 2025, 1198-1203HAL
23 inproceedingsN.Nicolas‌ Faroß and T.Thomas Sturm. On the‌ Number of Real Types of Univariate Polynomials.‌ISSAC '25: Proceedings of the 2025 International Symposium‌ on Symbolic and Algebraic ComputationISSAC 2025 -‌ 50th International Symposium on Symbolic and Algebraic Computation‌Guanajuato, MexicoACMNovember 2025, 62-69HAL‌DOI back to text
24 inproceedingsS.Simon‌ Guilloud, J.Julie Cailler, A.Auguste‌ Poiroux, Y.Yann Herklotz, T.Thomas‌ Bourgeat and V.Viktor Kunčak. Interoperability of‌ Proof Systems with SC-TPTP.CADE 30 -‌ 30th International Conference on Automated Deduction15943Lecture‌ Notes in Computer ScienceStuttgart, GermanySpringer Nature‌ SwitzerlandJuly 2025, 325-340HAL DOI back‌ to text
25 inproceedingsH.Hendrik Leidinger and‌ C.Christoph Weidenbach. Computing Ground Congruence Classes‌.Automated Deduction – CADE 30: 30th International‌ Conference on Automated Deduction, Stuttgart, Germany, July 28-31,‌ 2025, Proceedings15943Stuttgart, GermanyJuly 2025HAL‌back to text
26 inproceedingsBest paperV.‌Vincent Trélat. Safely Encoding B Proof Obligations‌ in SMT-LIB.Lecture Notes in Computer Science‌Rigorous State-Based Methods – 11th International Conference, ABZ‌ 202515728Düsseldorf, GermanySpringerJune 2025,‌ 52-69HAL DOI back to text back to‌ text

Conferences without proceedings

27 inproceedingsG.Ghilain‌ Bergeron, H.Horatiu Cirstea and S.Stephan‌ Merz. Towards a verified compiler for Distributed‌ PlusCal.11th International Workshop on Rewriting Techniques‌ for Program Transformations and EvaluationBirmingham, United Kingdom‌July 2025HAL back to text
28 inproceedings‌S.Stephan Merz. Invariant Synthesis: Decidable Fragments‌ to the Rescue.First-Order Reasoning, Below and‌ Beyond: Workshop in Honor of Christoph Weidenbach's 60th‌ BirthdayStuttgart, GermanyAugust 2025HAL

Scientific book‌ chapters

29 inbookI.Ivan Lanese, C.‌ A.Claudio Antares Mezzina and M.Martin Vassor‌. Bounded Reversibility in HOπ.16065Components‌ Operationally: Reversibility and System Engineering. Essays Dedicated to‌ Jean-Bernard Stefani on the Occasion of His 65th‌ BirthdayLecture Notes in Computer ScienceSpringer Nature‌ SwitzerlandOctober 2025, 24-45HAL DOI back‌ to text

Edition (books, proceedings, special issue of‌ a journal)

30 proceedingsC.Clark Barrett and‌ U.Uwe Waldmann, eds. Automated Deduction –‌ CADE 30.30th International Conference on Automated‌ Deduction15943Lecture Notes in Computer ScienceStuttgart,‌ Germany, GermanySpringer Nature Switzerland; Springer2025HAL‌DOI
31 proceedingsFrontiers of Combining Systems. 15th‌ International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29‌ – October 1, 2025, Proceedings.15th International‌ Symposium Frontiers of Combining Systems15979Lecture Notes‌ in Computer ScienceReykjavik, IcelandSpringer Nature Switzerland2026HAL DOI

Doctoral‌ dissertations and habilitation theses‌

32 thesisT.Thomas‌‌ Bagrel. Formalization and Implementation of Safe Destination‌ Passing in Pure Functional‌ Programming Settings.LORIA‌‌ (Université de Lorraine, CNRS, INRIA)November 2025HAL‌back to text back‌ to text back to‌‌ text back to text
33 thesisM.Martin‌ Desharnais. Formal verification‌ of logical calculi and‌‌ simulations in Isabelle/HOL.MPI for InformaticsJanuary‌ 2025HAL back to‌ text
34 thesisH.‌‌Hendrik Leidinger. SCL(EQ): Simple clause learning in‌ first-order logic with equality‌.MPI for Informatics‌‌May 2025HAL back to text

Reports &‌ preprints

35 miscN.‌Nathalie Bertrand, L.‌‌Loïc Hélouët, E.Engel Lefaucheux and L.‌Luca Paparazzo. Reachability‌ in multi-agent transfer systems‌‌ (Extended Version).November 2025HAL back to‌ text
36 miscN.‌Nicolas Faroß and T.‌‌Thomas Sturm. On the Number of Real‌ Types of Univariate Polynomials‌.2025HAL DOI‌‌

Scientific popularization

37 miscD.Dominique Méry.‌ Teaching formal techniques with‌ Event-B and Rodin ⋆‌‌.May 2025HALback to text

11.3‌ Cited publications

38 book‌J.-R.Jean-Raymond Abrial.‌‌ Modeling in Event-B: System and Software Engineering.‌Cambridge University Press2010‌back to text
39‌‌ inproceedingsR.Rajeev Alur, T. A.Thomas‌ A. Henzinger and M.‌ Y.Moshe Y. Vardi‌‌. Parametric real-time reasoning.Proc. 25th Annual‌ ACM Symp. Theory of‌ ComputingSan Diego, CA,‌‌ USAACM1993, 592-601back to text‌
40 articleL.Leo‌ Bachmair and H.Harald‌‌ Ganzinger. Rewrite-Based Equational Theorem Proving with Selection‌ and Simplification.Journal‌ of Logic and Computation‌‌431994, 217-247back to text‌
41 bookR.R.‌ Back and J.J.‌‌ von Wright. Refinement calculus---A systematic introduction.‌Springer Verlag1998back‌ to text
42 article‌‌N.Nathalie Bertrand, S.Serge Haddad and‌ E.Engel Lefaucheux.‌ A tale of two‌‌ diagnoses in probabilistic systems.Information and Computation‌2692019, 104441‌back to text
43‌‌ bookP.Patrick Blackburn, M. d.Maarten‌ de Rijke and Y.‌Yde Venema. Modal‌‌ Logic.Cambridge Tracts in Theoretical Computer Science‌Cambridge University Press2001‌DOI back to text‌‌
44 inproceedingsB.Bernard Boigelot, P.Pascal‌ Fontaine and B.Baptiste‌ Vergain. Non-emptiness Test‌‌ for Automata over Words Indexed by the Reals‌ and Rationals.Lecture‌ Notes in Computer Science‌‌15015Lecture Notes in Computer ScienceAkita, Japan‌Springer NatureSeptember 2024‌, 94-108HAL DOI‌‌back to text
45 inproceedingsG.Guillaume Bonfante‌, J.-P.Jean-Philippe Auzelle‌, R.Rémi Badonnel‌‌, S.Sébastien Duval, S.Stéphane Gégout‌, M.Marion Gilson‌, C.Clément Joliot‌‌, É.Éric Koessler, A.Audrey Knauf‌, N.Nicolas Krommenacker‌, S.Sébastien Schmitt‌‌ and P.Pierre Veutin. CyberHumanumEst, une guerre‌ cyber autour des Riverchelles‌.Rendez-Vous de la‌‌ Recherche et de l'Enseignement‌ de la Sécurité des Systèmes d'Information (RESSI) 2024‌Centre de Recherche en Informatique, Signal et Automatique‌ de Lille (Cristal, Université de Lile)Eppe-Sauvage, France‌May 2024HAL back to text
46 inproceedings‌A.Adel Bouhoula and M.Miki Hermann.‌ Primal Grammars Driven Automated Induction.Proceedings of‌ the Thirty-Third International Joint Conference on Artificial Intelligence‌Jeju, South KoreaAugust 2023, 3259-3269HAL‌DOI back to text
47 inproceedingsM.Martin‌ Bromberger, M.Martin Desharnais and C.Christoph‌ Weidenbach. An Isabelle/HOL Formalization of the SCL(FOL)‌ Calculus.Automated Deduction - CADE 29 -‌ 29th International Conference on Automated Deduction, Rome, Italy,‌ July 1-4, 2023, Proceedings14132Lecture Notes in‌ Computer ScienceSpringer2023, 116--133back to‌ text
48 inproceedingsM.Martin Bromberger, A.‌Alberto Fiori and C.Christoph Weidenbach. Deciding‌ the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by‌ Simple Clause Learning over Theories.Verification, Model‌ Checking, and Abstract Interpretation - 22nd International Conference,‌ VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings‌12597Lecture Notes in Computer ScienceSpringer2021‌, 511--533back to text
49 inproceedingsM.‌Martin Bromberger, C.Chaahat Jain and C.‌Christoph Weidenbach. SCL(FOL) Can Simulate Non-Redundant Superposition‌ Clause Learning.Automated Deduction - CADE 29‌ - 29th International Conference on Automated Deduction, Rome,‌ Italy, July 1-4, 2023, Proceedings14132Lecture Notes‌ in Computer ScienceSpringer2023, 134--152back‌ to text
50 inproceedingsD.David Déharbe,‌ P.Pascal Fontaine, Y.Yoann Guyot and‌ L.Laurent Voisin. SMT solvers for Rodin‌.ABZ - Third International Conference on Abstract‌ State Machines, Alloy, B, VDM, and Z -‌ 20127316Lecture Notes in Computer SciencePisa,‌ ItalySpringer2012, 194-207back to text‌
51 inproceedingsI.Isabela Drămnesc, E.Erika‌ Ábrahám, T.Tudor Jebelean, N.Nikolaos‌ Fachantidis, G.Gábor Kusper and S.Sorin‌ Stratulat. A European Project on AI-based Robotics‌.TALE2024 (International Conference on Teaching, Assessment and‌ Learning for Engineering)Bengalore, IndiaDecember 2024HAL‌back to text
52 articleG.Gabriel Ebner‌, J.Jasmin Blanchette and S.Sophie Tourret‌. Unifying Splitting.J. Autom. Reason.67‌22023, 16back to text
53‌ phdthesisM.Marek Košta. New Concepts for‌ Real Quantifier Elimination by Virtual Substitution.Saarland‌ UniversityGermany2016DOIback to text
54‌ articleN.Niclas Kruff, C.Christoph Lüders‌, O.Ovidiu Radulescu, T.Thomas Sturm‌ and S.Sebastian Walcher. Algorithmic Reduction of‌ Biological Networks with Multiple Time Scales.Mathematics‌ in Computer Science153September 2021,‌ 499 - 534HALDOI back to text‌
55 bookL.Leslie Lamport. Specifying Systems‌.Boston, Mass.Addison-Wesley2002back to text‌
56 articleN.Nicolas Le Novere, B.‌Benjamin Bornstein, A.Alexander Broicher, M.‌Melanie Courtot, M.Marco Donizelli, H.Harish Dharuri, L.‌Lu Li, H.‌Herbert Sauro, M.‌‌Maria Schilstra, B.Bruce Shapiro and others‌. BioModels Database: A‌ Free, Centralized Database of‌‌ Curated, Published, Quantitative Kinetic Models of Biochemical and‌ Cellular Systems.Nucleic‌ acids res.34suppl_1‌‌January 2006, D689-D691DOI back to text‌
57 articleH.Hanl‌ Lee and A.Angelyn‌‌ Lao. Transmission Dynamics and Control Strategies Assessment‌ of Avian Influenza A‌ (H5N6) in the Philippines‌‌.Infectious Disease Modelling32018, 35-59‌DOI back to text‌
58 articleH.Hendrik‌‌ Leidinger and C.Christoph Weidenbach. SCL(EQ): SCL‌ for First-Order Logic with‌ Equality.J. Autom.‌‌ Reason.6732023, 22back to‌ text
59 bookC.‌Carroll Morgan. Programming‌‌ from Specifications.2nd editionPrentice Hall1998‌back to text
60‌ inproceedingsD.Diego Ongaro‌‌ and J. K.John K. Ousterhout. In‌ Search of an Understandable‌ Consensus Algorithm.USENIX‌‌ Annual Technical Conference 2014Philadelphia, PAUsenix Association‌2014, 305-319back‌ to text
61 inproceedings‌‌C.Colin Rothgang, F.Florian Rabe and‌ C.Christoph Benzmüller.‌ Theorem Proving in Dependently-Typed‌‌ Higher-Order Logic.CADE14132Lecture Notes in‌ Computer ScienceSpringer2023‌, 438--455back to‌‌ text
62 inproceedingsH.-J.Hans-Jörg Schurr, M.‌Mathias Fleury, H.‌Haniel Barbosa and P.‌‌Pascal Fontaine. Alethe: Towards a Generic SMT‌ Proof Format (extended abstract)‌.Seventh Workshop on‌‌ Proof eXchange for Theorem Proving (PxTP 2021)336‌EPTCS2021, 49-54‌back to text
63‌‌ inproceedingsS.Sophie Tourret and J.Jasmin Blanchette‌. A modular Isabelle‌ framework for verifying saturation‌‌ provers.CPPACM2021, 224--237back‌ to text

VERIDIS - 2025

VERIDIS - 2025

2025Activity reportTeam﻿​﻿﻿VERIDIS

Keywords

Computer Science​‌﻿﻿ and Digital Science

Other Research Topics​‌﻿﻿ and Application Domains

1​‌﻿﻿ Team members, visitors, external​​﻿﻿ collaborators

Research Scientists

Faculty Members

Post-Doctoral Fellow

PhD Students

Interns and​​​‌ Apprentices

Administrative Assistants﻿﻿﻿‌

External Collaborator﻿​​﻿

2﻿﻿﻿‌ Overall objectives

3 Research program﻿‌​‌

3.1 Automated and Interactive﻿​​﻿ Theorem Proving

3.2 Formal Methods​‌﻿﻿ for Developing and Analyzing​​﻿﻿ Algorithms and Systems

Model checking.

Correctness by construction

3.3 Verification and​​​‌ Analysis of Dynamic Properties﻿﻿﻿‌ of Biological Systems

4 Application domains

5 Highlights of the﻿​​﻿ year

6 Latest﻿​​﻿ software developments, platforms, open​​​‌ data

6.1 Latest software﻿﻿﻿‌ developments

6.1.1 SPASS Workbench﻿‌​‌

6.1.2 Goeland

6.1.3​​​‌ E-Cyclist

6.1.4 TLAPS​‌﻿﻿

6.1.5 Logic1

6.1.6 Redlog﻿﻿﻿‌

6.2 New﻿​﻿﻿ platforms

6.2.1 ODEbase

7 New﻿​﻿﻿ results

7.1 Automated Deduction​‌﻿﻿ Techniques

Graph Superposition for​​﻿﻿ Quantum Circuits

Challenging Benchmarks for Circuit​​​‌ Equivalence Checks in SMT-LIB﻿﻿﻿‌ and TPTP

GNN for Word Equations​​​‌ Solving

A Framework for Certifying﻿﻿﻿‌ Tableaux Proofs in Rocq﻿‌​‌

Non-Ground Congruence​​﻿﻿ Closure

Decision procedures​​﻿﻿ for fragments with arithmetic.​​​‌

The​​​‌ SMT-LIB standard.

7.2 Interactive Theorem​‌﻿﻿ Proving

Formalizing the Relationship​​﻿﻿ Between SCL(FOL) and Ground​​​‌ Ordered Resolution

An Extension of the​​​‌ TPTP Derivation Format for﻿﻿﻿‌ Sequent-Based Calculi.

Integration of Abduction in﻿﻿﻿‌ Isabelle/HOL.

Formalization of Modal​​​‌ Model Theory in Isabelle/HOL﻿﻿﻿‌

Lean to DHOL Translation​​​‌

Certification of Rewriting​‌﻿﻿ on Circuits

Reconstruction﻿​﻿﻿ of SMT Proofs in​‌﻿﻿ Lambdapi.

An Isabelle/HOL framework to﻿﻿﻿‌ Add Splitting on Top﻿‌​‌ of Saturation Calculi

Towards the Verification of﻿​​﻿ ProVerif in Isabelle/HOL

Analysing the​​​‌ Divergence of Induction-based Proofs.﻿﻿﻿‌

A Verified Encoding​​​‌ of Proof Obligations.

7.3​​﻿﻿ Formal Methods for Developing​​​‌ and Analyzing Algorithms and﻿​﻿﻿ Systems

Formalization and Implementation​‌﻿﻿ of Safe Destination Passing​​﻿﻿ in Pure Functional Programming​​​‌ Settings.

Verified Code Generation﻿﻿﻿‌ from PlusCal Programs.

Gröbner Bases for​​​‌ Boolean Function Minimization.

Formalization and verification of​​﻿﻿ a train scheduler in​​​‌ TLA+.

Reversibility​​​‌ for Fault Tolerance in﻿​﻿﻿ Typed Sessions.

Bounded Reversibility in﻿​​﻿ HOπ

An inductive invariant﻿﻿﻿‌ for a high-level Raft﻿‌​‌ specification

7.4 Algorithmic Verification

Degradation​‌﻿﻿ of stochastic systems

Multi-agent transfer systems﻿​﻿﻿

7.5 Foundational Research﻿﻿﻿‌ in Arithmetic Reasoning

On﻿‌​‌ the number of real﻿​​﻿ types of univariate polynomials.​​​‌

8 Bilateral contracts and​‌﻿﻿ grants with industry

8.1​​﻿﻿ Bilateral contracts with industry​​​‌

Type​‌﻿﻿ systems for the memory​​﻿﻿ safety of functional programs​​​‌

Reengineering protocols for industrial​​​‌ controllers

Event-B modeling for﻿​﻿﻿ Human-Machine Interaction

9 Partnerships​‌﻿﻿ and cooperations

9.1 International​​﻿﻿ initiatives

9.1.1 Associate Teams​​​‌ in the framework of﻿​﻿﻿ an Inria International Lab​‌﻿﻿ or in the framework​​﻿﻿ of an Inria International​​​‌ Program

9.1.2 Participation in﻿﻿﻿‌ other International Programs

9.2 National﻿‌​‌ initiatives

ANR Project BiSoUS﻿​​﻿

ANR Project BLaSST​​​‌

ANR Project EBRP

2025Activity reportTeamVERIDIS

Computer Science‌ and Digital Science

Other Research Topics‌ and Application Domains

1‌ Team members, visitors, external collaborators

Interns and‌ Apprentices

Administrative Assistants‌

External Collaborator

2‌ Overall objectives

3 Research program‌‌

3.1 Automated and Interactive Theorem Proving

3.2 Formal Methods‌ for Developing and Analyzing Algorithms and Systems

3.3 Verification and‌ Analysis of Dynamic Properties‌ of Biological Systems

5 Highlights of the year

6 Latest software developments, platforms, open‌ data

6.1 Latest software‌ developments

6.1.1 SPASS Workbench‌‌

6.1.3‌ E-Cyclist

6.1.4 TLAPS‌

6.1.6 Redlog‌

6.2 New platforms

7 New results

7.1 Automated Deduction‌ Techniques

Graph Superposition for Quantum Circuits

Challenging Benchmarks for Circuit‌ Equivalence Checks in SMT-LIB‌ and TPTP

GNN for Word Equations‌ Solving

A Framework for Certifying‌ Tableaux Proofs in Rocq‌‌

Non-Ground Congruence Closure

Decision procedures for fragments with arithmetic.‌

The‌ SMT-LIB standard.

7.2 Interactive Theorem‌ Proving

Formalizing the Relationship Between SCL(FOL) and Ground‌ Ordered Resolution

An Extension of the‌ TPTP Derivation Format for‌ Sequent-Based Calculi.

Integration of Abduction in‌ Isabelle/HOL.

Formalization of Modal‌ Model Theory in Isabelle/HOL‌

Lean to DHOL Translation‌

Certification of Rewriting‌ on Circuits

Reconstruction of SMT Proofs in‌ Lambdapi.

An Isabelle/HOL framework to‌ Add Splitting on Top‌‌ of Saturation Calculi

Towards the Verification of ProVerif in Isabelle/HOL

Analysing the‌ Divergence of Induction-based Proofs.‌

A Verified Encoding‌ of Proof Obligations.

7.3 Formal Methods for Developing‌ and Analyzing Algorithms and Systems

Formalization and Implementation‌ of Safe Destination Passing in Pure Functional Programming‌ Settings.

Verified Code Generation‌ from PlusCal Programs.

Gröbner Bases for‌ Boolean Function Minimization.

Formalization and verification of a train scheduler in‌ TLA+.

Reversibility‌ for Fault Tolerance in Typed Sessions.

Bounded Reversibility in HO $π$

An inductive invariant‌ for a high-level Raft‌‌ specification

Degradation‌ of stochastic systems

Multi-agent transfer systems

7.5 Foundational Research‌ in Arithmetic Reasoning

On‌‌ the number of real types of univariate polynomials.‌

8 Bilateral contracts and‌ grants with industry

8.1 Bilateral contracts with industry‌

Type‌ systems for the memory safety of functional programs‌

Reengineering protocols for industrial‌ controllers

Event-B modeling for Human-Machine Interaction

9 Partnerships‌ and cooperations

9.1 International initiatives

9.1.1 Associate Teams‌ in the framework of an Inria International Lab‌ or in the framework of an Inria International‌ Program

9.1.2 Participation in‌ other International Programs

9.2 National‌‌ initiatives

ANR Project BiSoUS

ANR Project BLaSST‌

ANR Project‌‌ ICSPA

10.1‌ Promoting scientific activities

10.1.1 Scientific events:‌‌ organization

General chair, scientific chair

Member of organizing committees

10.1.2 Scientific events: selection

Member of‌ conference program committees

Editor in Chief

Member of the‌ editorial boards

Reviewer - reviewing activities

10.1.4 Invited talks

10.1.5 Leadership within the scientific community

10.1.7 Research administration

10.2 Teaching‌ - Supervision - Juries‌‌ - Educational and pedagogical outreach

10.2.4‌ Educational and pedagogical outreach‌