5 citations · 13 across the 8 of their papers we have counts for
6 papers · 1 filter
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…
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…
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…