Proof automation and type synthesis for set theory in the context of TLA+
Automatisation de preuves et synthèse de types pour la théorie des ensembles dans le contexte de TLA+
Résumé
This thesis presents effective techniques for discharging TLA+ proofobligations to automated theorem provers based on unsorted and many-sortedfirst-order logic. TLA+ is a formal language for specifying and verifyingconcurrent and distributed systems. Its non-temporal fragment is based on avariant of Zermelo-Fraenkel set theory for specifying the data structures. TheTLA+ Proof System TLAPS is an interactive proof environment in which users candeductively verify safety properties of TLA+ specifications. While TLAPS is aproof assistant that relies on users for guiding the proof effort, itgenerates proof obligations and passes them to backend verifiers to achieve asatisfactory level of automation.We developed a new back-end prover that soundly integrates into TLAPS externalautomated provers, specifically, ATP systems and SMT solvers. Two maincomponents provide the formal basis for implementing this new back-end. Thefirst is a generic translation framework that allows to plug to TLAPS anyautomated prover supporting the standard input formats TPTP/FOF orSMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets bycomprehension or total functions with domains, the translation to first-orderlogic relies on term-rewriting techniques coupled with an abstraction method.Sorted theories such as linear integer arithmetic are homomorphically embeddedinto many-sorted logic. The second component is a type synthesis algorithm for(untyped) TLA+ formulas. The algorithm, which is based on constraint solving,implements one type system for elementary types, similar to those ofmany-sorted logic, and an expansion with dependent and refinement types. Theobtained type information is then implicitly exploited to improve thetranslation. Empirical evaluation validates our approach: the ATP/SMT backendsignificantly boosts the proof development in TLAPS.
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.
Loading...