13 citations · 13 across the 3 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2022
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…
cs.PL2021
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…