82 citations · 214 across the 25 of their papers we have counts for
3 papers · 1 filter
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…
Demand-driven Alias Analysis : Formalizing Bidirectional Analyses for Soundness and Precision
Swati Jaiswal, Uday P. Khedker, Supratik Chakraborty
A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive…