6 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…
Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms
Derek Egolf, Stavros Tripakis
Synthesis of distributed protocols is a hard, often undecidable, problem. Completion techniques provide partial remedy by turning the problem into a search problem. However, the sp…
Decoupled Fitness Criteria for Reactive Systems
Derek Egolf, Stavros Tripakis
The correctness problem for reactive systems has been thoroughly explored and is well understood. Meanwhile, the efficiency problem for reactive systems has not received the same a…