BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:TLA+ Model Checking Made Symbolic
DTSTART:20191128T161500
DTEND:20191128T170000
DTSTAMP:20260506T165906Z
UID:66941f50907d22463283e6143399b5cd453ea160356989b1dc044319
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Igor Konnov\n\nBio\nIgor Konnov is a senior research scient
 ist at Interchain Foundation. He is developing model checking techniques f
 or parameterized and fault-tolerant distributed algorithms. He is a co-PI 
 in the project “APALACHE: Abstraction-based Parameterized Model Checker"
  funded by Vienna Science and Technology Fund (WWTF). Before joining Inter
 chain Foundation\, Igor Konnov worked as a researcher at Inria Nancy (Fran
 ce) and as a postdoc at TU Wien (Austria). He received his MSc and PhD in 
 Applied Mathematics and Computer Science from Lomonosov Moscow State Unive
 rsity (Russia).\n\nAbstract\nTLA+ is a language for formal specification o
 f all kinds of computer systems. System designers use this language to spe
 cify concurrent\, distributed\, and fault tolerant protocols\, which are t
 raditionally presented in pseudo-code. TLA+ is extremely concise yet expre
 ssive: The language primitives include Booleans\, integers\, functions\, t
 uples\, 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.\n\nIn this paper\, we presen
 t APALACHE – a first symbolic model checker for TLA+. Like TLC\, it assu
 mes that all specification parameters are fixed and all states are finite 
 structures. Unlike TLC\, APALACHE translates the underlying transition rel
 ation into quantifier-free SMT constraints\, which allows us to exploit th
 e power of SMT solvers. Designing this translation is the central challeng
 e that we address in this paper. Our experiments show that APALACHE outper
 forms TLC on examples with large state spaces.\n\nMore information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR