Zachary Kincaid 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 multi-threaded 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.

publications

Proof Spaces for Unbounded Parallelism with Azadeh Farzan and Andreas Podelski. To appear at 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.

Consistency Analysis of Decision-Making 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.
POPL14a PDF
PDF

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, 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 PDF
PDF
POPL14b Slides
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 SMT-based optimization algorithm for objective functions in the theory of linear real arithmetic.
POPL14c PDF
PDF

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.
CAV13b PDF
PDF

Recursive program synthesis with Aws Albargouthi and Sumit Gulwani. At 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
PDF

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.
POPL13 PDF
PDF
POPL13 Slides
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 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 PDF
PDF
POPL12 Slides
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.
SAS10 PDF
PDF
SAS10 Slides
Slides

Duplication in DNA sequences with Masami Ito, Lila Kari, and Shinnosuke Seki. At DLT 2008.
The duplication and repeat-deletion 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 repeat-deletions). 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.
DLT2008 PDF
PDF

service

the rest