4 papers
Can LLMs Perform Synthesis?
Derek Egolf, Yuhao Zhou, Stavros Tripakis
How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, dist…
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…