Proof automation and type synthesis for set theory in the context of TLA+

Résumé : Cette thèse présente des techniques efficaces pour déleguer des obligations depreuves TLA+ dans des démonstrateurs automatiques basées sur la logique dupremier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour laspécification et vérification des systèmes concurrents et distribués. Sapartie non-temporelle basée sur une variante de la théorie des ensemblesZermelo-Fraenkel permet de définir des structures de données. Le système depreuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequelles utilisateurs peuvent vérifier de manière deductive des propriétés desûreté sur des spécifications TLA+. TLAPS est un assistant de preuve quirepose sur les utilisateurs pour guider l’effort de preuve, il permet degénèrer des obligations de preuve puis les transmet aux vérificateursd’arrière-plan pour atteindre un niveau satisfaisant d’automatisation.Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègrecorrectement dans TLAPS des vérificateurs externes automatisés, enparticulier, des systèmes ATP et solveurs SMT. Deux principales composantesconstituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet deraccorder à TLAPS tout démonstrateur automatisé supportant les formatsstandards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordresupérieur, tels que les ensembles par compréhension ou des fonctionstotales avec des domaines, la traduction de la logique du premier ordrerepose sur des techniques de réécriture couplées à une méthode parabstraction. Les théories sortées telles que l’arithmétique linéairesont intégrés par injection dans la logique multi-sortée. La deuxièmecomposante est un algorithme pour la synthèse des types dans les formules(non-typées) TLA+. L’algorithme, qui est basé sur la résolution descontraintes, met en oeuvre un système de type avec types élémentaires,similaires à ceux de la logique multi-sortée, et une extension avec destypes dépendants et par raffinement. Les informations de type obtenues sontensuite implicitement exploitées afin d’améliorer la traduction. Cetteapproche a pu être validé empiriquement permettant de démontrer que lesvérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS.
Liste complète des métadonnées

Littérature citée [166 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01096518
Contributeur : Vanzetto Hernán <>
Soumis le : mercredi 17 décembre 2014 - 16:10:36
Dernière modification le : jeudi 5 octobre 2017 - 01:15:40
Document(s) archivé(s) le : lundi 23 mars 2015 - 15:40:24

Fichier

Identifiants

  • HAL Id : tel-01096518, version 1

Citation

Hernán Vanzetto. Proof automation and type synthesis for set theory in the context of TLA+. Computer Science [cs]. Université de Lorraine, 2014. English. 〈tel-01096518〉

Partager

Métriques

Consultations de la notice

546

Téléchargements de fichiers

449