TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states.
In this paper, we present APALACHE – a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, APALACHE translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers. Designing this translation is the central challenge that we address in this paper.
Our experiments show that APALACHE outperforms TLC on examples with large state spaces.
Fri 25 OctDisplayed time zone: Beirut change
14:00 - 15:30
|Value-Centric Dynamic Partial Order Reduction|
Krishnendu Chatterjee IST Austria, Andreas Pavlogiannis EPFL, Viktor Toman IST Austria (Institute of Science and Technology Austria)DOI
|Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency|
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Bengt Jonsson Uppsala University, Sweden, Magnus Lång Uppsala University, Sweden, Tuan Phong Ngo Uppsala University, Sweden, Konstantinos (Kostis) Sagonas Uppsala University, SwedenDOI Pre-print
|TLA+ Model Checking Made Symbolic|
Igor Konnov Inria Nancy - Grand Est, France, Jure Kukovec TU Wien, Austria, Thanh-Hai Tran TU Wien, AustriaDOI
|Effective Lock Handling in Stateless Model Checking|
Michalis Kokologiannakis MPI-SWS, Germany, Azalea Raad MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, GermanyDOI