Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Fri 25 Oct 2019 14:45 - 15:07 at Templars - Model Checking Chair(s): Casper Bach Poulsen

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 Oct
Times are displayed in time zone: (GMT+03:00) Beirut change

14:00 - 15:30: OOPSLA - Model Checking at Templars
Chair(s): Casper Bach PoulsenDelft University of Technology
splash-2019-oopsla14:00 - 14:22
Krishnendu ChatterjeeIST Austria, Andreas PavlogiannisEPFL, Viktor TomanIST Austria (Institute of Science and Technology Austria)
splash-2019-oopsla14:22 - 14:45
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Bengt JonssonUppsala University, Sweden, Magnus LångUppsala University, Sweden, Tuan Phong NgoUppsala University, Sweden, Konstantinos (Kostis) SagonasUppsala University, Sweden
DOI Pre-print
splash-2019-oopsla14:45 - 15:07
Igor KonnovInria Nancy - Grand Est, France, Jure KukovecTU Wien, Austria, Thanh-Hai TranTU Wien, Austria
splash-2019-oopsla15:07 - 15:30
Michalis KokologiannakisMPI-SWS, Germany, Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany