Zak Kincaid
I'm an assistant professor at Princeton University. My main research interests are in program analysis and programming languages. Email: zkincaid@cs.princeton.edu Office: Computer Science Building, Room 315 Address: 35 Olden Street, Princeton, NJ 08540 
news
 5/3: A Symbolic Decision Procedure for Symbolic Alternating Automata with Loris D'Antoni and Fang Wang accepted at MFPS 2017.
 2/13: Compositional Recurrence Analysis Revisited with Jason Breck, Ashkan Boroujeni, and Tom Reps accepted at PLDI 2017.
 2/6: In Spring 2017, I'm leading an independent work seminar on practical solutions for intractable problems.
 1/9: I'm serving on the program committee of VSTTE 2017.
selected publications (full list at dblp)
Compositional Recurrence Analysis Revisited
with Jason Breck, Ashkan Boroujeni, and Tom Reps.
Compositional recurrence analysis (CRA) is a staticanalysis method
based on a combination of symbolic analysis and abstract
interpretation. CRA computes the meaning of a procedure following
Tarjan’s pathexpression 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
contextfreelanguage underpinnings of contextsensitive 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.


Slides 
Proving Liveness of Parameterized Programs
with Azadeh Farzan and Andreas Podelski.
LICS 2016.
Correctness of multithreaded 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.


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


Slides 
Spatial Interpolants
with Aws Albarghouthi,
Josh Berdine, and
Byron Cook.
ESOP 2015.
We propose SplInter, a new technique for proving properties of
heapmanipulating programs that marries (1) a new separation
logicbased analysis for heap reasoning with (2) an
interpolationbased technique for refining heapshape 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 multithreaded 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.


Slides 
Consistency Analysis of DecisionMaking 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, handwritten 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.


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 SMTbased 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 inputoutput examples has the power of extending
the range of computational tasks achievable by endusers who have no
programming knowledge, but can articulate their desired computations by
describing inputoutput behaviour. In this paper we present Escher, an
algorithm that interacts with the user via inputoutput 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.


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.


Slides 
Verification of parameterized concurrent programs by modular reasoning about data and control
with Azadeh Farzan.
POPL 2012.
We consider the problem of verifying threadstate 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. 

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.


Slides 
teaching
In Spring 2017, I am teaching COS IW 08: Practical solutions to intractable problems. Past: Fall 2016  COS 597D: Reasoning about concurrent systems.
activities
 (Upcoming) VSTTE 2017: Program Committee.
 CAV 2017: Program Committee.
 PLDI 2017: Program Committee.
 POPL 2017: Program Committee.
 CAV 2016: Workshop chair/Program Committee.
 PLDI 2016: External Review Committee.
 TACAS 2016: Program Committee.
 SSS 2015: Program Committee
 Tiny Transactions on Computer Science vol. 3.: Program Committee
 PLDI 2014: Artifact Evaluation Committee
the rest
 I received my PhD at the University of Toronto. My adviser was Azadeh Farzan.
 Some of my work is implemented in the Duet program analyzer.
 What I'm listening to.
 My Erdős number is 3.
 Chinmay Narayan has typeset a FAQ for our POPL12 paper.