I am a computer science Ph.D. student at the University of Wisconsin-Madison. My advisor is 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.
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\).
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).
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.