I am a computer science Ph.D. student at the University of Wisconsin-Madison. My advisor is Thomas Reps.

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.

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\).

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).

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.

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

- I am currently taking 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 I am very proud of 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.
- According to spotify, my top artists include Jimi Hendrix, Weezer, Led Zeppelin, Childish Gambino, Eric B. & Rakim, Miles Davis, Johnny Cash, Lady Gaga, The White Stripes, and Daft Punk.
- I like playing the guitar in my free time. I am trying to get better at blues improvisation, so if anyone has good resources let me know.