Jason Breck

Software Engineer

University of Wisconsin-Madison

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

he/him/his



About Me

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.


Publications

PLDI 2020 Templates and Recurrences: Better Together
Breck, Cyphert, Kincaid, 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(nlog2(7)).
CAV 2019 Proving Unrealizability for Syntax-Guided Synthesis
Hu, Breck, Cyphert, D'Antoni, 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 (PG), such that, if a standard program-analysis tool can establish that a certain assertion in (PG) always holds, then the synthesis problem is unrealizable.
POPL 2019 Refinement of Path Expressions for Static Analysis
Cyphert, Breck, Kincaid, 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.
POPL 2019 Closed Forms for Numerical Loops
Kincaid, Breck, Cyphert, 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).
POPL 2018 Non-linear Reasoning for Invariant Synthesis
Kincaid, Cyphert, Breck, 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.
PLDI 2017 Compositional Recurrence Analysis Revisited
Kincaid, Breck, Forouhi Boroujeni, Reps
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
Miné, Breck, Reps
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
Thakur, Breck, Reps
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.