COLTELLACCI ALESSIO | Doctorat UL

26/01

14h00

Soutenance de thèse de ALESSIO COLTELLACCI

Reconstruction des preuves SMT dans Lambdapi

Reconstructing SMT Proofs in Lambdapi

Jury

Directeur de these_MERZ_Stephan_Université de Lorraine
Examinateur_KELLER_Chantal_LMF, Université Paris-Saclay
Examinateur_FLEURY_Mathias_University of Freiburg
Examinateur_LALEAU_Régine_Université Paris-Est Créteil
Rapporteur_KOVáCS_Laura_ TU Wien
Rapporteur_STEEN_Alexander_University of Greifswald

école doctorale

IAEM - INFORMATIQUE - AUTOMATIQUE - ELECTRONIQUE - ELECTROTECHNIQUE - MATHEMATIQUES

Laboratoire

LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Mention de diplôme

Informatique

A008 Loria Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy

Mots clés

Type dépendant,SMT,LambdaPi,Alethe,TLA+,Raisonnement automatisé

Résumé de la thèse

Les prouveurs automatiques de théorèmes modernes sont de plus en plus puissants et largement utilisés pour établir la correction de systèmes informatiques critiques. Parmi eux, les solveurs SMT (Satisfiabilité Modulo Théories) jouent un rôle central grâce à leur expressivité et leur efficacité dans la gestion de tâches de raisonnement logique complexes.

Keywords

Dependent type,SMT,LambdaPi,Alethe,TLA+,Automated reasoning

Abstract

Powerful modern automated theorem provers are increasingly used to establish the correctness of critical computer systems. Among them, Satisfiability Modulo Theories (SMT) solvers play a central role thanks to their expressive power and efficiency in handling complex logical reasoning tasks.

Liste de toutes les soutenances