13 citations · 23 across the 10 of their papers we have counts for
3 papers · 1 filter
Optimal Stateless Model Checking of Transactional Programs under Causal Consistency
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ashutosh Gupta +2
We present a framework for efficient stateless model checking (SMC) of concurrent programs under five prominent models of causal consistency, CCv,CM,CC, Read Committed and Read Ato…
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…