Graduated computer science Ph.D. from the University of Wisconsin-Madison. My advisor was Thomas Reps.

Some Links

Papers

Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis@POPL 2024 [ Talk ]

John Cyphert and Zachary Kincaid

This paper presents a monotone program analysis method that generates program invariants involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops.

Optimal Symbolic Bound Synthesis on arXiv

John Cyphert, Yotam Feldman, Zachary Kincaid, and Thomas Reps

The problem of finding a constant bound on a term given a set of assumptions has wide applications in optimization as well as program analysis. However, in many contexts the objective term may be unbounded. Still, some sort of symbolic bound may be useful. In this paper we introduce the optimal symbolic-bound synthesis problem, and a technique that tackles this problem for non-linear arithmetic with function symbols. This allows us to automatically produce symbolic bounds on complex arithmetic expressions from a set of both equality and inequality assumptions. Our solution employs a novel combination of powerful mathematical objects -- Gröbner bases together with polyhedral cones -- to represent an infinite set of implied inequalities. We obtain a sound symbolic bound by reducing the objective term by this infinite set. We implemented our method in a tool, AutoBound, which we tested on problems originating from real Solidity programs. We find that AutoBound yields relevant bounds in each case, matching or nearly-matching upper bounds produced by a human analyst on the same set of programs.

Algebraic Program Analysis Tutorial Paper @CAV 2021

Zachary Kincaid, Thomas Reps, and John Cyphert

This paper is a tutorial on algebraic program analysis. It explains the foundations of algebraic program analysis, its strengths and limitations, and gives examples of algebraic program analyses for numerical invariant generation and termination analysis.

Synthesis with Asymptotic Resource Bounds @CAV 2021

Qinheping Hu, John Cyphert, Loris D' Antoni, and Thomas Reps

We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity \(O(n\log(n))\). Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, \(SynPlexity\), was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.

Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems @PLDI 2020

Qinheping Hu, John Cyphert, Loris D' Antoni, and Thomas Reps

We again consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable. However, in this work we present an algorithm for exactly solving a set of equations that result from SyGuS problems over linear integer arithmetic (LIA) and LIA with conditionals (CLIA), thereby showing that LIA and CLIA SyGuS problems over finitely many examples are decidable. We implemented the proposed technique and algorithms in a tool called Nay. Nay can prove unrealizability for 70/132 existing SyGuS benchmarks, with running times comparable to those of the state-of-the-art tool Nope. Moreover, Nay can solve 11 benchmarks that Nope cannot solve.

Templates and Recurrences: Better Together @PLDI 2020

Jason Breck, John Cyphert, Zachary Kincaid, and Thomas Reps

This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. In this paper, we combine these two approaches and obtain a technique that uses templates in which the unknowns are functions rather than numbers, and the constraints on the unknowns are recurrences. The technique synthesizes invariants involving polynomials, exponentials, and logarithms, even in the presence of arbitrary control-flow, including any combination of loops, branches, and (possibly non-linear) recursion. For instance, it is able to show that (i) the time taken by merge-sort is \(O(n\log(n))\), and (ii) the time taken by Strassen's algorithm is \(O(n^{log_2(7)})\).

Proving Unrealizability for Syntax-Guided Synthesis @CAV 2019 [ slides ]

Qinheping Hu, Jason Breck, John Cyphert, Loris D' Antoni, and Thomas Reps

We consider the problem of automatically establishing that a given syntax-guided-synthesis (\(SyGuS\)) problem is unrealizable (i.e., has no solution). We reduce the unrealizability problem to a reachability problem by encoding the synthesis problem's grammar \(G\) as a nondeterministic program \(P_G\), such that, if a standard program-analysis tool can establish that a certain assertion in \(P_G\) always holds, then the synthesis problem is unrealizable.

Refinement of Path Expressions for Static Analysis @POPL 2019 [ slides ]

John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps

Algebraic program analyses compute information about a program's behavior by first (a) computing a valid path expression and then (b) interpreting the path expression in a semantic algebra that defines the analysis. There are an infinite number of different regular expressions that qualify as valid path expressions, which raises the question: ''Which one should we choose?'' While any choice yields a sound result, for many analyses the choice can have a drastic effect on the precision of the results obtained. In this paper, we develop an algorithm that takes as input a valid path expression \(E\), and returns a valid path expression \(E'\) that is guaranteed to yield analysis results that are at least as good as those obtained using \(E\).

Closed Forms for Numerical Loops @POPL 2019 [ slides ]

Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps

This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing these closed forms is decidable. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).

Non-Linear Reasoning for Invariant Synthesis @POPL 2018 [ slides ]

Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps

This paper presents a method for generating non-linear invariants for general loops (conditional branches, nested loops, non-deterministic assignments, etc.) by analyzing recurrence relations. The key components are an abstract domain for reasoning about non-linear arithmetic, a semantics-based method for extracting recurrence relations from loop bodies, and a recurrence solver that avoids closed forms that involve complex or irrational numbers.

Awards

2020 Google Ph.D. Fellowship

Workshops

Guarantees in Program Synthesis @SYNT 2019

Qinheping Hu, Jason Breck, John Cyphert, Loris D' Antoni, and Thomas Reps

Presentations

Algebraic Program Analysis @MWPLS 2019

Service

Proceedings and Talks Coordinator @CAV 2021

Some Things

  • I completed a set of classes to get my Ph.D. minor in economics.
  • I gave a series of lectures to the madPL seminar on the basics of category theory. You can view some typeset notes here. The last set of notes is incomplete. I will try and finish it sometime in the future.
  • I am originally from Shelby, Ohio. I received my undergraduate degree from The Ohio State University in 2016.