17 citations · 48 across the 18 of their papers we have counts for
4 papers · 1 filter
Reductions for Safety Proofs (Extended Version)
Azadeh Farzan, Anthony Vandikas
Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplif…
Reductions for Automated Hypersafety Verification
Azadeh Farzan, Anthony Vandikas
We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation…
Modular Synthesis of Divide-and-Conquer Parallelism for Nested Loops (Extended Version)
Azadeh Farzan, Victor Nicolet
We propose a methodology for automatic generation of divide-and-conquer parallel implementations of sequential nested loops. We focus on a class of loops that traverse read-only mu…
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner +1
We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how t…