5 citations · 13 across the 8 of their papers we have counts for
10 papers
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Zachary Kincaid, Nicolas Koh, Shaowei Zhu
This paper presents a theory of non-linear integer/real arithmetic and algorithms for reasoning about this theory. The theory can be conceived as an extension of linear integer/rea…
Reflections on Termination of Linear Loops
Shaowei Zhu, Zachary Kincaid
This paper shows how techniques for linear dynamical systems can be used to reason about the behavior of general loops. We present two main results. First, we show that every loop…
Termination Analysis Without the Tears
Shaowei Zhu, Zachary Kincaid
Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis are divided into two groups: (1) algorithms with stron…
Templates and Recurrences: Better Together
Jason Breck, John Cyphert, Zachary Kincaid +1
This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. A t…
Loop Summarization with Rational Vector Addition Systems (extended version)
Jake Silverman, Zachary Kincaid
This paper presents a technique for computing numerical loop summaries. The method synthesizes a rational vector addition system with resets (Q-VASR) that simulates the action of a…
A Symbolic Decision Procedure for Symbolic Alternating Finite Automata
Loris D'Antoni, Zachary Kincaid, Fang Wang
We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean…
Proving Liveness of Parameterized Programs
Azadeh Farzan, Zachary Kincaid, Andreas Podelski
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,…
Compositional Invariant Generation via Linear Recurrence Analysis
Azadeh Farzan, Zachary Kincaid
This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input/output relation o…
Spatial Interpolants
Aws Albarghouthi, Josh Berdine, Byron Cook +1
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 inte…
An Algebraic Framework for Compositional Program Analysis
Azadeh Farzan, Zachary Kincaid
The purpose of a program analysis is to compute an abstract meaning for a program which approximates its dynamic behaviour. A compositional program analysis accomplishes this task…