Zachary Kincaid
I am a Computer Science Ph.D. student at the University of Toronto. My advisor is Azadeh Farzan. Email: zkincaid@cs.toronto.edu Office: Bahen Centre Rm 3232 
my research
I am interested in program analysis and verification. My work is focused on generating invariants and proving safety properties for concurrent programs. This work is based on abstracting away the flow of control of multithreaded programs (an essentially sequential concept) and analyzing the flow of data (an essentially parallel concept) instead. In other words: I work on parallel proofs for parallel programs!Some of my work is implemented in the Duet program analyzer.
news
 5/19: In Fall 2016, I will join Princeton University as an assistant professor!
 1/7: I'm on the program committee of SSS 2015.
 12/16: I'm on the program committee of TACAS 2016.
publications
Spatial Interpolants
with Aws Albarghouthi,
Josh Berdine, and
Byron Cook.
To appear at 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.
At 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.
At 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.
At 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.
At 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.
At 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.
At 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.
At 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.
At 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. At 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 
Duplication in DNA sequences
with Masami Ito, Lila Kari, and Shinnosuke Seki.
At DLT 2008.
The duplication and repeatdeletion operations are the basis of a
formal language theoretic model of errors that can occur during DNA
replication. During DNA replication, subsequences of a strand of DNA
may be copied several times (resulting in duplications) or skipped
(resulting in repeatdeletions). In this paper, we investigate several
properties of these operations, including closure properties of
language families in the Chomsky hierarchy, equations involving these
operations, and steps towards a characterization of regular duplication
languages, i.e. languages that are the result of the duplication
operation applied to a given set.


service
 Upcoming: Program Committee, Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2016. Consider submitting!
 Program Committee, International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS) 2015.
 Program Committee, Tiny Transactions on Computer Science vol. 3.
 Artifact Evaluation Committee, Programming Languages Design and Implementation (PLDI) 2014.
the rest
 My DBLP entry.
 What I'm listening to.
 My Erdős number is 3.
 The background of this page is an iDFG proof of Lamport's bakery algorithm.
 Chinmay Narayan has typeset a FAQ for our POPL12 paper.