| 2024 | CAV | Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement. | Charlie Murphy, Zachary Kincaid |
| 2024 | CAV | Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates. | Shaowei Zhu, Zachary Kincaid |
| 2024 | SIGCOMM | Relational Network Verification. | Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David Walker, Ennan Zhai |
| 2021 | CAV | Algebraic Program Analysis. | Zachary Kincaid, Thomas W. Reps, John Cyphert |
| 2021 | CAV | Reflections on Termination of Linear Loops. | Shaowei Zhu, Zachary Kincaid |
| 2021 | PLDI | Termination analysis without the tears. | Shaowei Zhu, Zachary Kincaid |
| 2020 | PLDI | Templates and recurrences: better together. | Jason Breck, John Cyphert, Zachary Kincaid, Thomas W. Reps |
| 2019 | CAV | Loop Summarization with Rational Vector Addition Systems. | Jake Silverman, Zachary Kincaid |
| 2019 | VMCAI | A Practical Algorithm for Structure Embedding. | Charlie Murphy, Zachary Kincaid |
| 2018 | SAS | Numerical Invariants via Abstract Machines. | Zachary Kincaid |
| 2017 | CONCUR | A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk). | Azadeh Farzan, Zachary Kincaid |
| 2017 | PLDI | Compositional recurrence analysis revisited. | Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas W. Reps |
| 2016 | IJCAI | Linear Arithmetic Satisfiability via Strategy Improvement. | Azadeh Farzan, Zachary Kincaid |
| 2016 | LICS | Proving Liveness of Parameterized Programs. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2015 | ESOP | Spatial Interpolants. | Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid |
| 2015 | FMCAD | Compositional Recurrence Analysis. | Azadeh Farzan, Zachary Kincaid |
| 2015 | LATA | Automated Program Verification. | Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid, Andreas Podelski |
| 2015 | POPL | Proof Spaces for Unbounded Parallelism. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2014 | POPL | Consistency analysis of decision-making programs. | Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid |
| 2014 | POPL | Proofs that count. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2014 | POPL | Symbolic optimization with SMT solvers. | Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik |
| 2013 | CAV | Recursive Program Synthesis. | Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid |
| 2013 | CAV | Duet: Static Analysis for Unbounded Parallelism. | Azadeh Farzan, Zachary Kincaid |
| 2013 | POPL | Inductive data flow graphs. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2012 | POPL | Verification of parameterized concurrent programs by modular reasoning about data and control. | Azadeh Farzan, Zachary Kincaid |
| 2010 | SAS | Compositional Bitvector Analysis for Concurrent Programs with Nested Locks. | Azadeh Farzan, Zachary Kincaid |
| 2008 | DLT | Duplication in DNA Sequences. | Masami Ito, Lila Kari, Zachary Kincaid, Shinnosuke Seki |