My Publications
Publications
Higher Category Theory
Papers
Duality for weak $\omega$-categories.
2024.
@misc{benjamin2024duality,
title={Duality for weak $\omega$-categories},
author={Thibaut Benjamin and Ioannis Markakis},
year={2024},
eprinttype={arXiv},
eprint={2402.01611},
doi={10.48550/arXiv.2402.01611},
primaryClass={math.CT},
pdf={http://thibautbenjamin.github.io/papers/duality2024.pdf},
abstract={We define inductively the opposites of a weak globular
ω-category with respect to a set of dimensions, and
we show that the properties of being free on a
globular set of a computad are preserved under
forming opposites. We then provide a new description
of hom ω-categories, and show that the opposites of
a hom ω-category are hom ω-category of opposites of
the original ω-category. },
}
We define inductively the opposites of a weak globular
ω-category with respect to a set of dimensions, and
we show that the properties of being free on a
globular set of a computad are preserved under
forming opposites. We then provide a new description
of hom ω-categories, and show that the opposites of
a hom ω-category are hom ω-category of opposites of
the original ω-category.
Formalisation of Dependent Type Theory: The Example of CaTT.
In
27th International Conference on Types for Proofs and Programs (TYPES 2021),
Leibniz International Proceedings in Informatics (LIPIcs),
Volume
239,
Basold, Henning and Cockx, Jesper and Ghilezan, Silvia,
Schloss Dagstuhl – Leibniz-Zentrum für Informatik,
pages:
2:1–2:21,
2022.
@InProceedings{benjamin21formalization,
author={Benjamin, Thibaut},
title={{Formalisation of Dependent Type Theory: The Example of CaTT}},
booktitle={27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages={2:1--2:21},
series={Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN={978-3-95977-254-9},
ISSN={1868-8969},
year={2022},
volume={239},
editor={Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
addres ={Dagstuhl, Germany},
URL={https://drops.dagstuhl.de/opus/volltexte/2022/16771},
URN={urn:nbn:de:0030-drops-167719},
doi={10.4230/LIPIcs.TYPES.2021.2},
annote={Keywords: Dependent type theory, homotopy type theory, higher categories, formalisation, Agda, proof assistant},
eprinttype={arXiv},
eprint={2111.14736},
pdf={http://thibautbenjamin.github.io/papers/types2021.pdf},
abstract={We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak omega-categories,
and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is
well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and
thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of
these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent
to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific
side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory
CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation
provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak omega-categories. The article
is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present. },
}
We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak omega-categories,
and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is
well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and
thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of
these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent
to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific
side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory
CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation
provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak omega-categories. The article
is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present.
Monoidal weak omega-categories as models of a type theory.
In
Mathematical Structures in Computer Science,
Cambridge University Press,
pages:
1–37,
2022.
@article{benjamin22monoidal,
title={Monoidal weak omega-categories as models of a type theory},
doi={10.1017/S0960129522000172},
journal={Mathematical Structures in Computer Science},
publisher={Cambridge University Press},
author={Benjamin, Thibaut},
year={2022},
eprinttype = {arXiv},
eprint= {2111.14208},
pages={1--37},
pdf={http://thibautbenjamin.github.io/papers/mscs2022.pdf},
slides={http://thibautbenjamin.github.io/slides/2019lhc.pdf},
abstract={Weak omega-categories are notoriously difficult to define because of the very intricate nature of their axioms.
Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of
weak omega-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this
definition of globular weak omega-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type
theory called 𝖢𝖺𝖳𝖳 , whose models are weak omega-categories. Here, we generalize this approach to monoidal weak omega-categories.
Based on the principle that they should be equivalent to weak omega-categories with only one 0-cell, we are able to derive a type theory 𝖬𝖢𝖺𝖳𝖳
whose models are monoidal weak omega-categories. This requires changing the rules of the theory in order to encode the information carried by
the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory 𝖬𝖢𝖺𝖳𝖳
and the type theory 𝖢𝖺𝖳𝖳 . Our main contribution is to show that these translations relate the models of our type theory to the models of
the type theory 𝖢𝖺𝖳𝖳 consisting of omega-categories with only one 0-cell by analyzing in details how the notion of models interact with
the structural rules of both type theories.},
}
Weak omega-categories are notoriously difficult to define because of the very intricate nature of their axioms.
Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of
weak omega-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this
definition of globular weak omega-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type
theory called 𝖢𝖺𝖳𝖳 , whose models are weak omega-categories. Here, we generalize this approach to monoidal weak omega-categories.
Based on the principle that they should be equivalent to weak omega-categories with only one 0-cell, we are able to derive a type theory 𝖬𝖢𝖺𝖳𝖳
whose models are monoidal weak omega-categories. This requires changing the rules of the theory in order to encode the information carried by
the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory 𝖬𝖢𝖺𝖳𝖳
and the type theory 𝖢𝖺𝖳𝖳 . Our main contribution is to show that these translations relate the models of our type theory to the models of
the type theory 𝖢𝖺𝖳𝖳 consisting of omega-categories with only one 0-cell by analyzing in details how the notion of models interact with
the structural rules of both type theories.
Globular weak omega-categories as models of a type theory.
2024.
Accepted in Higher Structures
@article{benjamin21globular,
doi={10.48550/ARXIV.2106.04475},
author={Benjamin, Thibaut and Finster, Eric and Mimram, Samuel},
title={Globular weak omega-categories as models of a type theory},
eprinttype={arXiv},
eprint={2106.04475},
year={2024},
pdf={http://thibautbenjamin.github.io/papers/hs2021.pdf},
slides={http://thibautbenjamin.github.io/slides/2022cirm.pdf},
notes={Accepted in Higher Structures},
abstract={We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak omega-categories,
following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a
formal proof that the models of this type theory correspond precisely to weak omega-categories, as defined by Maltsiniotis, by generalizing
a definition proposed by Grothendieck for weak omega-groupoids: those are defined as suitable presheaves over a cat-coherator,
which is a category encoding structure expected to be found in an omega-category. This comparison is established by proving
the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for
a certain class of dependent type theories},
}
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak omega-categories,
following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a
formal proof that the models of this type theory correspond precisely to weak omega-categories, as defined by Maltsiniotis, by generalizing
a definition proposed by Grothendieck for weak omega-groupoids: those are defined as suitable presheaves over a cat-coherator,
which is a category encoding structure expected to be found in an omega-category. This comparison is established by proving
the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for
a certain class of dependent type theories
Globular weak omega-categories as models of a type theory.
2021.
Accepted at the workshop on Homotopy Type Theory / Univalent Foundations
@unpublished{benjamin21hottuf,
author = {Benjamin, Thibaut and Finster, Eric and Mimram, Samuel},
title = {{Globular weak omega-categories as models of a type theory}},
notes = {Accepted at the workshop on Homotopy Type Theory / Univalent Foundations},
year = {2021},
keywords = {rewriting,submitted},
pdf = {http://thibautbenjamin.github.io/papers/hottuf2021.pdf},
slides={http://thibautbenjamin.github.io/slides/2021hottuf.pdf},
}
Suspension et Fonctorialité: Deux Opérations Implicites Utiles en CaTT.
In
Journées Francophones des Langages Applicatifs,
2019.
In French
@inproceedings{benjamin2019suspension,
title = {Suspension et Fonctorialit{\'e}: Deux Op{\'e}rations Implicites Utiles en CaTT},
author = {Benjamin, Thibaut and Mimram, Samuel},
booktitle = {Journ{\'e}es Francophones des Langages Applicatifs},
year = {2019},
url = {https://hal.inria.fr/hal-01985195/},
eprinttype={hal},
eprint={hal-01985195},
notes={In French},
slides={http://thibautbenjamin.github.io/slides/2019jfla.pdf},
abstract={La notion de omega-catégorie faible est une vaste généralisation de celle de catégorie, qui revêt une importance croissante en mathématiques.
Cependant, les définitions qui en ont été proposées à ce jour à ce jour restent difficiles à manipuler en pratique : on ne connaît
pas de liste explicite des cohérences qui doivent être présentes dans ces structures et il devient rapidement difficile de vérifier
tous les détails qui doivent l’être lors de leur utilisation. Partant de ce constat, Finster et Mimram ont récemment reformulé la définition
de Grothendieck et Maltsiniotis des omega-catégories faibles sous forme d’une théorie des types, appelée CaTT. Ceci a posé les bases
d’un assistant de preuve, développé par les auteurs, dans lequel les termes typables sont ceux qui correspondent à des cohérences.
La formalisation de preuves non-triviales dans ce système a montré la nécessité d’avoir des outils permettant de les automatiser
en partie. Dans cette optique, nous présentons ici deux méthodes permettant de générer automatiquement des cohérences de
dimension supérieure à partir de cohérences existantes : la suspension et la fonctorialité. Nous montrons qu’elles sont
admissibles (c’est-à-dire que leur présence ne modifie pas le pouvoir expressif de la théorie des types) et qu’elles sont utiles en
pratique pour alléger les preuves en évitant des redondances.},
}
La notion de omega-catégorie faible est une vaste généralisation de celle de catégorie, qui revêt une importance croissante en mathématiques.
Cependant, les définitions qui en ont été proposées à ce jour à ce jour restent difficiles à manipuler en pratique : on ne connaît
pas de liste explicite des cohérences qui doivent être présentes dans ces structures et il devient rapidement difficile de vérifier
tous les détails qui doivent l’être lors de leur utilisation. Partant de ce constat, Finster et Mimram ont récemment reformulé la définition
de Grothendieck et Maltsiniotis des omega-catégories faibles sous forme d’une théorie des types, appelée CaTT. Ceci a posé les bases
d’un assistant de preuve, développé par les auteurs, dans lequel les termes typables sont ceux qui correspondent à des cohérences.
La formalisation de preuves non-triviales dans ce système a montré la nécessité d’avoir des outils permettant de les automatiser
en partie. Dans cette optique, nous présentons ici deux méthodes permettant de générer automatiquement des cohérences de
dimension supérieure à partir de cohérences existantes : la suspension et la fonctorialité. Nous montrons qu’elles sont
admissibles (c’est-à-dire que leur présence ne modifie pas le pouvoir expressif de la théorie des types) et qu’elles sont utiles en
pratique pour alléger les preuves en évitant des redondances.
My PhD Thesis
A type theoretic approach to weak omega-categories and related higher structures.
2020.
@phdthesis{benjamin:tel-03106197,
title={{A type theoretic approach to weak omega-categories and related higher structures}},
author={Benjamin, Thibaut},
url={https://tel.archives-ouvertes.fr/tel-03106197},
number={2020IPPAX077},
school={{Institut Polytechnique de Paris}},
year={2020},
month=Nov,
keywords={Type theory ; Higher categories ; Category theory ; Pasting schemes ; Semantics ; Homotopy type theory ; Th{\'e}orie des types ; Cat{\'e}gories sup{\'e}rieures ; Th{\'e}orie des cat{\'e}gories ; Diagrammes de compositions ; S{\'e}mantique ; Th{\'e}orie homotopique des types},
type={Theses},
eprinttype={hal},
eprint={tel-03106197},
pdf={https://tel.archives-ouvertes.fr/tel-03106197/file/94836_BENJAMIN_2020_archivage.pdf},
abstract={We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from
ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The
advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules,
it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a
proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two
main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories,
and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider
a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent
type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of
categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics
of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition
of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable
of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation
together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version.
To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and
the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We
then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to
allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a
connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of
higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able
to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal
weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models:
It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the
correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak
omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous
presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics,
our main result along these lines is to characterize the models of this type theory and extract a mathematical definition
equivalent to them. },
}
We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from
ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The
advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules,
it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a
proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two
main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories,
and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider
a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent
type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of
categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics
of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition
of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable
of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation
together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version.
To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and
the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We
then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to
allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a
connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of
higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able
to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal
weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models:
It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the
correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak
omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous
presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics,
our main result along these lines is to characterize the models of this type theory and extract a mathematical definition
equivalent to them.
Runtime Assertion Checking
Abstract Interpretation of Recursive Logic Definitions for
Efficient Runtime Assertion Checking.
In
International Conference on Tests and Proofs (TAP),
Best Paper Award.
2023.
@inproceedings{benjamin23tap,
author = {Benjamin, Thibaut and Signoles, Julien},
title = {{Abstract Interpretation of Recursive Logic Definitions for
Efficient Runtime Assertion Checking}},
booktitle = {International Conference on Tests and Proofs (TAP)},
year = 2023,
month = jul,
pdf = {http://thibautbenjamin.github.io/papers/tap2023.pdf},
slides = {http://thibautbenjamin.github.io/slides/tap2023.pdf},
note = {Accepted for publication},
bestpaper = {Best Paper Award},
abstract = {Runtime Assertion Checking (RAC) is a lightweight formal method
for verifying at runtime code properties written in a formal specification
language. One of the main challenge of RAC is to check the properties
efficiently, while emitting sound verdicts. In particular, arithmetic
properties are only efficiently verified using machine integers, yet
soundness can only be achieved by using an exact but slower exact arithmetic
library.
This paper presents how E-ACSL, a RAC tool for C programs, applies
abstract interpretation for efficiently and soundly supporting arithmetic
properties. Abstract interpretation provides
sound static information regarding the size of terms involved in
runtime assertions in order to choose at compile time whether
machine integers or exact arithmetic will be used at runtime on a case by case
basis. Our specification language includes recursive user-defined logic
functions and predicates, for which we rely on fast fixpoint operators based
on widening of abstract values.}
}
Runtime Assertion Checking (RAC) is a lightweight formal method
for verifying at runtime code properties written in a formal specification
language. One of the main challenge of RAC is to check the properties
efficiently, while emitting sound verdicts. In particular, arithmetic
properties are only efficiently verified using machine integers, yet
soundness can only be achieved by using an exact but slower exact arithmetic
library.
This paper presents how E-ACSL, a RAC tool for C programs, applies
abstract interpretation for efficiently and soundly supporting arithmetic
properties. Abstract interpretation provides
sound static information regarding the size of terms involved in
runtime assertions in order to choose at compile time whether
machine integers or exact arithmetic will be used at runtime on a case by case
basis. Our specification language includes recursive user-defined logic
functions and predicates, for which we rely on fast fixpoint operators based
on widening of abstract values.
Formalizing an Efficient Runtime Assertion Checker for an
Arithmetic Language with Functions and Predicates.
In
Symposium On Applied Computing (SAC),
2023.
@inproceedings{benjamin23sac,
author = {Benjamin, Thibaut and Signoles, Julien},
title = {{Formalizing an Efficient Runtime Assertion Checker for an
Arithmetic Language with Functions and Predicates}},
booktitle = {Symposium On Applied Computing (SAC)},
year = 2023,
month = mar,
pdf = {http://thibautbenjamin.github.io/papers/sac2023.pdf},
slides = {http://thibautbenjamin.github.io/slides/sac2023.pdf},
abstract = {Runtime Assertion Checking (RAC) is a lightweight formal method
that verifies formal code annotations, typically assertions, at runtime.
The main RAC challenge consists in generating code that is both
sound and efficient for checking expressive properties. In
particular, checking formal arithmetic properties usually requires
to use machine integer arithmetic to be efficient, but needs to rely
on an exact yet slower arithmetic library to be sound.
This paper formalizes an efficient RAC tool for arithmetic
properties, which may include user-defined functions and predicates.
Efficient code generation for these routines is based on
specialization, allowing to generate efficient functions using
machine arithmetic when possible, or slower functions relying on
exact arithmetic, according to the calling context. This
formalization is implemented in E-ACSL, a runtime assertion checker
for C programs.}
}
Runtime Assertion Checking (RAC) is a lightweight formal method
that verifies formal code annotations, typically assertions, at runtime.
The main RAC challenge consists in generating code that is both
sound and efficient for checking expressive properties. In
particular, checking formal arithmetic properties usually requires
to use machine integer arithmetic to be efficient, but needs to rely
on an exact yet slower arithmetic library to be sound.
This paper formalizes an efficient RAC tool for arithmetic
properties, which may include user-defined functions and predicates.
Efficient code generation for these routines is based on
specialization, allowing to generate efficient functions using
machine arithmetic when possible, or slower functions relying on
exact arithmetic, according to the calling context. This
formalization is implemented in E-ACSL, a runtime assertion checker
for C programs.
Formalisation d’un vérificateur efficace d’assertions
arithmétiques à l’exécution.
In
Journées Francophones des Langages Applicatifs (JFLA’22),
2022.
In French
@inproceedings{benjamin22jfla,
author = {Benjamin, Thibaut and Ridoux, F\'elix and Signoles, Julien},
title = {Formalisation d'un v\'erificateur efficace d'assertions
arithmétiques \`a l'ex\'ecution},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA'22)},
year = 2022,
eprinttype={hal},
eprint={hal-03626779},
notes={In French},
pdf={http://thibautbenjamin.github.io/papers/jfla2022.pdf},
slides={http://thibautbenjamin.github.io/slides/2022jfla.pdf},
abstract = {La vérification d'assertions à l'exécution est une technique
consistant à vérifier la validité d'annotations formelles pendant l'exécution
d'un programme. Bien qu'ancienne, cette technique reste encore peu étudiée
d'un point de vue théorique. Cet article contribue à pallier ce manque en
formalisant un vérificateur d'assertions à l'exécution pour des propriétés
arithmétiques entières. La principale difficulté réside dans la modélisation
d'un générateur de code pour les propriétés visées qui génère du code à la
fois correct et efficace. Ainsi, le code généré repose sur des entiers
machines lorsque le générateur peut prouver qu'il est correct de le faire et
sur une bibliothèque spécialisée dans l'arithmétique exacte, correcte mais
moins efficace, dans les autres cas. Il utilise pour cela un système de
types dédié. En outre, la logique considérée pour les propriétés inclue des
constructions d'ordre supérieur. L'article présente également une
implémentation de ce générateur de code au sein d'E-ACSL, le greffon de
Frama-C dédié à la vérification d'assertions à l'exécution, ainsi qu'une
première évaluation expérimentale démontrant empiriquement l'efficacité du
code généré.}
}
La vérification d’assertions à l’exécution est une technique
consistant à vérifier la validité d’annotations formelles pendant l’exécution
d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée
d’un point de vue théorique. Cet article contribue à pallier ce manque en
formalisant un vérificateur d’assertions à l’exécution pour des propriétés
arithmétiques entières. La principale difficulté réside dans la modélisation
d’un générateur de code pour les propriétés visées qui génère du code à la
fois correct et efficace. Ainsi, le code généré repose sur des entiers
machines lorsque le générateur peut prouver qu’il est correct de le faire et
sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais
moins efficace, dans les autres cas. Il utilise pour cela un système de
types dédié. En outre, la logique considérée pour les propriétés inclue des
constructions d’ordre supérieur. L’article présente également une
implémentation de ce générateur de code au sein d’E-ACSL, le greffon de
Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une
première évaluation expérimentale démontrant empiriquement l’efficacité du
code généré.