Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
Abstract
We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference technique to work directly on TLA+, an expressive, high level specification language. To achieve this, we present a new algorithm for invariant inference that is based around a core procedure for generating plain, potentially non-inductive lemma invariants that are used as candidate conjuncts of an overall inductive invariant. We couple this with a greedy lemma invariant selection procedure that selects lemmas that eliminate the largest number of counterexamples to induction at each round of our inference procedure. We have implemented our algorithm in a tool, endive, and evaluate it on a diverse set of distributed protocol benchmarks, demonstrating competitive performance and ability to uniquely solve an industrial scale reconfiguration protocol.
Cite
@article{arxiv.2205.06360,
title = {Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+},
author = {William Schultz and Ian Dardik and Stavros Tripakis},
journal= {arXiv preprint arXiv:2205.06360},
year = {2022}
}