Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction

Derek Egolf, Stavros Tripakis

We present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA+. Our method's chief novelty lies in a new search space red…