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

Hernán Vanzetto 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadatas

Cited literature [166 references]  Display  Hide  Download

https://hal.inria.fr/tel-01751181
Contributor : Vanzetto Hernán <>
Submitted on : Wednesday, December 17, 2014 - 4:10:36 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Monday, March 23, 2015 - 3:40:24 PM

Identifiers

  • HAL Id : tel-01751181, version 2

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. ⟨NNT : 2014LORR0208⟩. ⟨tel-01751181v2⟩

Share

Metrics

Record views

726

Files downloads

756