BmcMT: Bounded Model Checking of TLA + Specifications with SMT

Abstract : We present the development version of BmcMT—a symbolic model checker for TLA+. It finds, whether a TLA+ specification satisfies an invariant candidate by checking satisfiability of an SMT formula that encodes: (1) an execution of bounded length, and (2) preservation of the invariant candidate in every state of the execution. Our tool is still in the experimental phase, due to a number of challenges posed by TLA+ semantics to SMT solvers. We will discuss these challenges and our current approach to them in the talk. Our preliminary experiments show that BmcMT scales better than the standard TLA+ model checker TLC for large parameter values, e.g., when a TLA+ specification models a system of 10 processes, though TLC is more efficient for tiny parameters, e.g., when the system has 3 processes. We believe that early feedback from the TLA+ community will help us to focus on the most important language features and improve our tool.
Type de document :
Document associé à des manifestations scientifiques
TLA+ Community Meeting 2018, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées

https://hal.inria.fr/hal-01899719
Contributeur : Igor Konnov <>
Soumis le : vendredi 19 octobre 2018 - 17:15:23
Dernière modification le : samedi 20 octobre 2018 - 01:13:51

Fichier

kkt18-bmcmt.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01899719, version 1

Collections

Citation

Igor Konnov, Jure Kukovec, Thanh Tran. BmcMT: Bounded Model Checking of TLA + Specifications with SMT. TLA+ Community Meeting 2018, Jul 2018, Oxford, United Kingdom. 〈hal-01899719〉

Partager

Métriques

Consultations de la notice

39

Téléchargements de fichiers

11