4 papers · 1 filter
Towards Language Model Guided TLA+ Proof Automation
Yuhao Zhou, Stavros Tripakis
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language mod…
Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
Derek Egolf, Stavros Tripakis
We present a novel approach for the synthesis of recursive programs from mixed-quantifier first-order logic properties. We solve this problem using a sketching-based, enumerative,…
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…
Efficient Synthesis of Symbolic Distributed Protocols by Sketching
Derek Egolf, William Schultz, Stavros Tripakis
We present a novel and efficient method for synthesis of parameterized distributed protocols by sketching. Our method is both syntax-guided and counterexample-guided, and utilizes…