Non-linear reasoning for invariant synthesis. - Zachary Kincaid; John Cyphert; Jason Breck; Thomas W. Reps (Proc. ACM Program. Lang., 2018)

Proving Unrealizability for Syntax-Guided Synthesis. - Qinheping Hu; Jason Breck; John Cyphert; Loris D'Antoni; Thomas W. Reps (CAV (1), 2019)

Refinement of path expressions for static analysis. - John Cyphert; Jason Breck; Zachary Kincaid; Thomas W. Reps (Proc. ACM Program. Lang., 2019)

Closed forms for numerical loops. - Zachary Kincaid; Jason Breck; John Cyphert; Thomas W. Reps (Proc. ACM Program. Lang., 2019)

Templates and recurrences: better together. - Jason Breck; John Cyphert; Zachary Kincaid; Thomas W. Reps (PLDI, 2020)

Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. - Qinheping Hu; John Cyphert; Loris D'Antoni; Thomas W. Reps (PLDI, 2020)

Synthesis with Asymptotic Resource Bounds. - Qinheping Hu; John Cyphert; Loris D'Antoni; Thomas W. Reps (CAV (1), 2021)

Algebraic Program Analysis. - Zachary Kincaid; Thomas W. Reps; John Cyphert (CAV (1), 2021)

Optimal Symbolic Bound Synthesis. - John Cyphert; Yotam Feldman; Zachary Kincaid; Thomas W. Reps (CoRR, 2023)

Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. - John Cyphert; Zachary Kincaid (Proc. ACM Program. Lang., 2024)