1 citations · 3 across the 3 of their papers we have counts for
6 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…
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,…