Skip to Main content Skip to Navigation
New interface
Documents associated with scientific events

BmcMT: Bounded Model Checking of TLA + Specifications with SMT

Igor Konnov 1, 2 Jure Kukovec 3 Thanh Hai Tran 3 
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
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
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.
Document type :
Documents associated with scientific events
Complete list of metadata

Cited literature [3 references]  Display  Hide  Download
Contributor : Igor Konnov Connect in order to contact the contributor
Submitted on : Friday, October 19, 2018 - 5:15:23 PM
Last modification on : Saturday, June 25, 2022 - 7:46:08 PM
Long-term archiving on: : Sunday, January 20, 2019 - 3:58:59 PM


Files produced by the author(s)


  • HAL Id : hal-01899719, version 1



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



Record views


Files downloads