13 citations · 13 across the 3 of their papers we have counts for
4 papers
Full-Program Induction: Verifying Array Programs sans Loop Invariants
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging…
Diffy: Inductive Reasoning of Array Programs using Difference Invariants
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
We present a novel verification technique to prove interesting properties of a class of array programs with a symbolic parameter N denoting the size of arrays. The technique relies…
Verifying Array Manipulating Programs with Full-Program Induction
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. In…
Verifying Array Manipulating Programs by Tiling
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a…