References & Citations
Computer Science > Logic in Computer Science
Title: Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
(Submitted on 12 May 2022 (v1), last revised 1 Oct 2022 (this version, v2))
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.
Submission history
From: William Schultz [view email][v1] Thu, 12 May 2022 20:53:44 GMT (57kb)
[v2] Sat, 1 Oct 2022 15:43:09 GMT (121kb)
Link back to: arXiv, form interface, contact.