Refinement Types for TLA+

Stephan Merz 1 Hernán Vanzetto 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MSR - INRIA - Microsoft Research - Inria Joint Centre
Abstract : TLA+ is a specification language, mainly intended for concurrent and distributed systems. Its non-temporal fragment is based on a variant of (untyped) ZF set theory. Motivated by the integration of the TLA+ Proof System with SMT solvers or similar tools based on multi-sorted first-order logic, we define a type system for TLA+ and we prove its soundness. The system includes refinement types, which fit naturally in set theory. Combined with dependent function types, we obtain type annotations on top of an untyped specification language, getting the best of both the typed and untyped approaches. After implementing the type inference algorithm, we show that the resulting typing discipline improves the verification capabilities of the proof system.
Type de document :
Communication dans un congrès
Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp.143-157, 2014, LNCS. 〈10.1007/978-3-319-06200-6_11〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01063516
Contributeur : Stephan Merz <>
Soumis le : vendredi 12 septembre 2014 - 11:57:28
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Stephan Merz, Hernán Vanzetto. Refinement Types for TLA+. Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp.143-157, 2014, LNCS. 〈10.1007/978-3-319-06200-6_11〉. 〈hal-01063516〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

294

Contact


archive-ouverte@inria.fr