Zachary Kincaid Zak Kincaid

I'm an assistant professor at Princeton University.
My main research interests are in program analysis and programming languages.
Office: Computer Science Building, Room 315
Address: 35 Olden Street, Princeton, NJ 08540


selected publications (full list at dblp)

Compositional Recurrence Analysis Revisited with Jason Breck, Ashkan Boroujeni, and Tom Reps.
Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. CRA computes the meaning of a procedure following Tarjan’s path-expression method: first compute a regular expression recognizing a set of paths through the procedure, then interpret that regular expression within a suitable semantic algebra. This paper introduces ICRA, an extension of CRA to recursive procedures. ICRA overcomes the “impedance mismatch” between CRA, which relies on representing program paths with regular languages, and the context-free-language underpinnings of context-sensitive analysis.

Linear Arithmetic Satisfiability via Strategy Improvement with Azadeh Farzan. IJCAI 2016.
This article presents a decision procedure for the theory of linear rational arithmetic (and linear integer arithmetic), including quantifiers. The algorithm is based on synthesizing winning strategies for quantified formulas (interpreted as satisfiability games) by mutual strategy improvement.
IJCAI16 Slides

Proving Liveness of Parameterized Programs with Azadeh Farzan and Andreas Podelski. LICS 2016.
Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program.
LICS16 Slides

Compositional Recurrence Analysis with Azadeh Farzan. FMCAD 2015.
This paper presents a new method for automatically generating numerical invariants for imperative programs. The procedure computes a transition formula which over-approximates the behaviour of a given input program. It is compositional in the sense that it operates by decomposing the program into parts, computing a transition formula for each part, and then composing them. Transition formulas for loops are computed by extracting recurrence relations from a transition formula for the loop body and then computing their closed forms. Experimentation demonstrates that this method is competitive with leading verification techniques.
FMCAD15 Slides

Spatial Interpolants with Aws Albarghouthi, Josh Berdine, and Byron Cook. ESOP 2015.
We propose SplInter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic-based analysis for heap reasoning with (2) an interpolation-based technique for refining heap-shape invariants with data invariants. SplInter is property directed, precise, and produces counterexample traces when a property does not hold. Using the novel notion of spatial interpolants modulo theories, SplInter can infer complex invariants over general recursive predicates, e.g., of the form "all elements in a linked list are even" or "a binary tree is sorted."

Proof Spaces for Unbounded Parallelism with Azadeh Farzan and Andreas Podelski. POPL 2015.
In this paper, we describe proof spaces, a proof system for verifying safety properties for multi-threaded programs in which the number of executing threads is not statically bounded. Our development of this proof system is motivated by the question of how to generalize a proof of correctness (perhaps obtained from a verifier for sequential programs) of a some finite set of example traces so that the correctness argument applies to all traces of the program. We show that proof spaces are complete relative to the inductive assertion method, and give algorithms for automating them.
POPL15 Slides

Consistency Analysis of Decision-Making Programs with Swarat Chaudhuri and Azadeh Farzan. POPL 2014.
Applications in many areas of computing make discrete decisions under uncertainty; for example, the application may rely on limited numerical precision in input, or on input or sensory data. While an application executing under uncertainty cannot be relied upon to make decisions which are correct with respect to a given world, it is desirable that their decisions are at least consistent (i.e., correct with respect to some possible world). This paper presents a sound, automatic program analysis for verifying program consistency.

Proofs that count with Azadeh Farzan and Andreas Podelski. POPL 2014.
Counting arguments are among the most basic methods of proof in mathematics. Within the field of formal verification, they are useful for reasoning about programs with infinite control, such as programs with an unbounded number of threads, or (concurrent) programs with recursive procedures. While counting arguments are common in informal, hand-written proofs of such programs, there are no fully automated techniques to construct counting arguments. The key questions involved in automating counting arguments are: how to decide what should be counted?, and how to decide when a counting argument is valid? In this paper, we present a technique for automatically constructing and checking counting arguments, which includes novel solutions to these questions.
POPL14b Slides

Symbolic Optimization with SMT solvers with Yi Li, Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik. POPL 2014.
The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in programming languages: software verification, program synthesis, functional programming, refinement types, etc. SMT solvers are effective at finding arbitrary satisfying assignments for formulae, but for some applications it is necessary to find an assignment that optimizes (minimizes/maximizes) certain criteria. We present an efficient SMT-based optimization algorithm for objective functions in the theory of linear real arithmetic.

Duet: static analysis for unbounded parallelism with Azadeh Farzan. CAV 2013.
Duet is a static analysis tool for concurrent programs in which the number of executing threads is not statically bounded. It has a modular architecture, which is based on separating the invariant synthesis problem in two subtasks: (1) data dependence analysis, which is used to construct a data flow model of the program, and (2) interpretation of the data flow model over a (possibly infinite) abstract domain, which generates invariants. This separation of concerns allows researchers working on data dependence analysis and abstract domains to combine their efforts toward solving the challenging problem of static analysis for unbounded concurrency.

Recursive program synthesis with Aws Albargouthi and Sumit Gulwani. CAV 2013.
Program synthesis from input-output examples has the power of extending the range of computational tasks achievable by end-users who have no programming knowledge, but can articulate their desired computations by describing input-output behaviour. In this paper we present Escher, an algorithm that interacts with the user via input-output examples to synthesize recursive programs. Escher is parameterized by the components that can be used in the program, thus providing a generic synthesis algorithm that can be instantiated to suit different domains. Escher adopts a novel search strategy through the space of programs that utilizes special datastructures for inferring conditionals and synthesizing recursive procedures.
CAV2013a PDF

Inductive data flow graphs with Azadeh Farzan and Andreas Podelski. POPL 2013.
We propose inductive data flow graphs, data flow graphs with incorporated inductive assertions, as the basis of an approach to verifying concurrent programs. An inductive data flow graph accounts for a set of dependencies between program events, and therefore stands as a representation for the set of executions which give rise to these dependencies. By representing information about dependencies rather than control flow, inductive data flow graphs can yield very succinct proofs. Our strategy for verifying concurrent programs defers reasoning about control to the proof checking step, a purely combinatorial problem, thus avoiding the need to reason about data and control simultaneously.
POPL13 Slides

Verification of parameterized concurrent programs by modular reasoning about data and control with Azadeh Farzan. POPL 2012.
We consider the problem of verifying thread-state properties of multithreaded programs in which the number of active threads cannot be statically bounded. Our approach is based on decomposing the task into two modules, where one reasons about data and the other reasons about control. The two modules are incorporated into a feedback loop, so that the abstractions of data and control are iteratively coarsened as the algorithm progresses (that is, they become weaker) until a fixed point is reached.
This version fixes some typographical errors that appeared in the printed version - thanks to Chinmay Narayan, Suvam Mukherjee, and Deepak D'Souza for finding them.
POPL12 Slides

Compositional bitvector analysis for concurrent programs with nested locks
with Azadeh Farzan. SAS 2010.
We propose a new technique for bitvector data flow analysis for concurrent programs. Our algorithm works for concurrent programs that synchronize via nested locks. We give a compositional algorithm that first computes thread summaries and then efficiently combines them to solve the dataflow analysis problem. We show that this algorithm computes precise solutions (meet over all paths) to bitvector problems.
SAS10 Slides


In Spring 2017, I am teaching COS IW 08: Practical solutions to intractable problems. Past:


the rest