Software Engineer

University of Wisconsin-Madison

j<last-name>@cs.wisc.edu

he/him/his

In December of 2020, I began working as a software engineer at Google.

In the fall of 2020, I obtained my PhD from the Department of Computer Sciences at the University of Wisconsin-Madison. My adviser was Tom Reps. My main area of research was static analysis (specifically, numerical invariant generation), with some connections to logic, complexity analysis, security, and program synthesis.

PLDI 2020
Templates and Recurrences: Better Together

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^{log2(7)}).

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

CAV 2019
Proving Unrealizability for Syntax-Guided Synthesis

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.

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

POPL 2019
Refinement of Path Expressions for Static Analysis

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.

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.

POPL 2019
Closed Forms for Numerical Loops

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

POPL 2018
Non-linear Reasoning for Invariant Synthesis

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.

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.

PLDI 2017
Compositional Recurrence Analysis Revisited

Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural version of CRA that handles recursive procedures. The problem is non-trivial because there is an "impedance mismatch" between CRA, which relies on analysis techniques based on regular languages (i.e., Tarjan's path-expression method), and the context-free-language underpinnings of context-sensitive analysis. We show how to address this impedance mismatch by augmenting the CRA abstract domain with additional operations. We call the resulting algorithm Interprocedural CRA (ICRA).

Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural version of CRA that handles recursive procedures. The problem is non-trivial because there is an "impedance mismatch" between CRA, which relies on analysis techniques based on regular languages (i.e., Tarjan's path-expression method), and the context-free-language underpinnings of context-sensitive analysis. We show how to address this impedance mismatch by augmenting the CRA abstract domain with additional operations. We call the resulting algorithm Interprocedural CRA (ICRA).

ESOP 2016
An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs

This paper addresses the problem of proving a given invariance property of a loop in a numeric program, by inferring automatically a stronger inductive invariant. The algorithm we present is based on both abstract interpretation and constraint solving. As in abstract interpretation, it computes the effect of a loop using a numeric abstract domain. As in constraint satisfaction, it works from "above"â€”interactively splitting and tightening a collection of abstract elements until an inductive invariant is found. (Nominated for the EASST Best-Paper Award at ETAPS 2016.)

This paper addresses the problem of proving a given invariance property of a loop in a numeric program, by inferring automatically a stronger inductive invariant. The algorithm we present is based on both abstract interpretation and constraint solving. As in abstract interpretation, it computes the effect of a loop using a numeric abstract domain. As in constraint satisfaction, it works from "above"â€”interactively splitting and tightening a collection of abstract elements until an inductive invariant is found. (Nominated for the EASST Best-Paper Award at ETAPS 2016.)

SPIN 2014
Satisfiability Modulo Abstraction for Separation Logic with Linked Lists

Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes points-to assertions (x |-> y), acyclic-list-segment assertions (ls(x,y)), logical-and, logical-or, separating conjunction, and septraction (the DeMorgan-dual of separating implication). The fragment that we consider allows negation at leaves, and includes formulas that lie outside other separation-logic fragments considered in the literature. The semi-decision procedure is designed using concepts from abstract interpretation. The procedure uses an abstract domain of shape graphs to represent a set of heap structures, and computes an abstraction that over-approximates the set of satisfying models of a given formula. If the over-approximation is empty, then the formula is unsatisfiable.

Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes points-to assertions (x |-> y), acyclic-list-segment assertions (ls(x,y)), logical-and, logical-or, separating conjunction, and septraction (the DeMorgan-dual of separating implication). The fragment that we consider allows negation at leaves, and includes formulas that lie outside other separation-logic fragments considered in the literature. The semi-decision procedure is designed using concepts from abstract interpretation. The procedure uses an abstract domain of shape graphs to represent a set of heap structures, and computes an abstraction that over-approximates the set of satisfying models of a given formula. If the over-approximation is empty, then the formula is unsatisfiable.