My Publications
Publications
Higher Category Theory
Papers
Invertible cells in ω-categories.
2024.
@online{benjamin_invertibility_2024,
title={Invertible cells in ω-categories},
author={Thibaut Benjamin and Ioannis Markakis},
year={2024},
pdf={http://thibautbenjamin.github.io/papers/invertibility2024.pdf},
abstract={ We study coinductive invertibility of cells in weak
ω-categories. We use the inductive presentation of
weak ω-categories via an adjunction with the
categroy of computads, and show that invertible
cells are closed under all operations of
ω-categories. Moreover, we give a simple criterion
for invertibility in computads, together with an
algorithm computing the data witnessing the
invertibility, including the inverse, and the
cancellation data. },
}
We study coinductive invertibility of cells in weak
ω-categories. We use the inductive presentation of
weak ω-categories via an adjunction with the
categroy of computads, and show that invertible
cells are closed under all operations of
ω-categories. Moreover, we give a simple criterion
for invertibility in computads, together with an
algorithm computing the data witnessing the
invertibility, including the inverse, and the
cancellation data.
CaTT contexts are finite computads.
2024.
@online{benjamin_catt_2024,
title={CaTT contexts are finite computads},
author={Thibaut Benjamin and Ioannis Markakis and Chiara Sarti},
year={2024},
eprinttype = {arXiv},
eprint={2405.00398},
doi={10.48550/arXiv.2405.00398},
url = {https://arxiv.org/abs/2405.00398},
pdf={http://thibautbenjamin.github.io/papers/catt-vs-computads.pdf},
abstract={Two novel descriptions of weak ω-categories have been
recently proposed, using type-theoretic ideas. The
first one is the dependent type theory CaTT whose
models are ω-categories. The second is a recursive
description of a category of computads together with
an adjunction to globular sets, such that the
algebras for the induced monad are again
ω-categories. We compare the two descriptions by
showing that there exits a fully faithful morphism
of categories with families from the syntactic
category of CaTT to the opposite of the category of
computads, which gives an equivalence on the
subcategory of finite computads. We derive a more
direct connection between the category of models of
CaTT and the category of algebras for the monad on
globular sets, induced by the adjunction with
computads. },
}
Two novel descriptions of weak ω-categories have been
recently proposed, using type-theoretic ideas. The
first one is the dependent type theory CaTT whose
models are ω-categories. The second is a recursive
description of a category of computads together with
an adjunction to globular sets, such that the
algebras for the induced monad are again
ω-categories. We compare the two descriptions by
showing that there exits a fully faithful morphism
of categories with families from the syntactic
category of CaTT to the opposite of the category of
computads, which gives an equivalence on the
subcategory of finite computads. We derive a more
direct connection between the category of models of
CaTT and the category of algebras for the monad on
globular sets, induced by the adjunction with
computads.
Opposites of weak ω-categories and the suspension and hom
adjunction.
2024.
@misc{benjamin2024duality,
title={Opposites of weak ω-categories and the suspension and hom
adjunction},
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
ω-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 ω-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
ω-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 ω-categories. The article is
accompanied by a development in the proof assistant
Agda to actually check the formalisation that we
present.
Monoidal weak ω-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 ω-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 ω-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 ω-groupoid in a globular setting,
since every type carries such a structure. Starting
from this remark, Brunerie could extract this
definition of globular weak ω-groupoids, formulated
as a type theory. By refining its rules, Finster and
Mimram have then defined a type theory called 𝖢𝖺𝖳𝖳 ,
whose models are weak ω-categories. Here, we
generalize this approach to monoidal weak
ω-categories. Based on the principle that they
should be equivalent to weak ω-categories with only
one 0-cell, we are able to derive a type theory
𝖬𝖢𝖺𝖳𝖳 whose models are monoidal weak ω-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
ω-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 ω-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 ω-groupoid in a globular setting,
since every type carries such a structure. Starting
from this remark, Brunerie could extract this
definition of globular weak ω-groupoids, formulated
as a type theory. By refining its rules, Finster and
Mimram have then defined a type theory called 𝖢𝖺𝖳𝖳 ,
whose models are weak ω-categories. Here, we
generalize this approach to monoidal weak
ω-categories. Based on the principle that they
should be equivalent to weak ω-categories with only
one 0-cell, we are able to derive a type theory
𝖬𝖢𝖺𝖳𝖳 whose models are monoidal weak ω-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
ω-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 ω-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 ω-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 ω-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
ω-categories, as defined by Maltsiniotis, by
generalizing a definition proposed by Grothendieck
for weak ω-groupoids: those are defined as suitable
presheaves over a cat-coherator, which is a category
encoding structure expected to be found in an
ω-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 ω-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
ω-categories, as defined by Maltsiniotis, by
generalizing a definition proposed by Grothendieck
for weak ω-groupoids: those are defined as suitable
presheaves over a cat-coherator, which is a category
encoding structure expected to be found in an
ω-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 ω-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 ω-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 ω-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 ω-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 ω-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 ω-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é.