Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+

William Schultz, Ian Dardik, Stavros Tripakis

We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference tec…