7 papers
Complete Local Reasoning About Parameterized Programs Over Topologies (Extended Version)
Ruotong Cheng, Azadeh Farzan
This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to…
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
Constantin Enea, Azadeh Farzan, Dominik Klumpp
The verification of reductions, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syn…
Parametrizing Reads-From Equivalence for Predictive Monitoring
Azadeh Farzan, Umang Mathur
Predictive runtime monitoring asks whether an execution of a concurrent program can be used to \emph{soundly predict} the existence of a reordering of that satisfies…
Symmetric Proofs of Parameterized Programs
Ruotong Cheng, Azadeh Farzan
We investigate the problem of safety verification of infinite-state parameterized programs that are formed based on a rich class of topologies. We introduce a new proof system, cal…
Products of Recursive Programs for Hypersafety Verification (Extended Version)
Ruotong Cheng, Azadeh Farzan
We study the problem of automated hypersafety verification of infinite-state recursive programs. We propose an infinite class of product programs, specifically designed with recurs…
Enhanced Data Race Prediction Through Modular Reasoning
Zhendong Ang, Azadeh Farzan, Umang Mathur
There are two orthogonal methodologies for efficient prediction of data races from concurrent program runs: commutativity and prefix reasoning. There are several instances of each…