18 citations · 30 across the 8 of their papers we have counts for
8 papers
Mizzle: A Complete Concurrent Incorrectness Logic with Applications to Agentic Bug Certification
Alexandre Moine, Sam Westrick, Joseph Tassarotti
Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers' time. We propose to prevent th…
A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, Joseph Tassarotti
We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time comp…
TypeDis: A Type System for Disentanglement
Alexandre Moine, Stephanie Balzer, Alex Xu +1
Disentanglement is a runtime property of parallel programs guaranteeing that parallel tasks remain oblivious to each other's allocations. As demonstrated in the MaPLe compiler and…
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
Alexandre Moine, Sam Westrick, Joseph Tassarotti
Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel…
Local Optimization of Quantum Circuits (Extended Version)
Jatin Arora, Mingkuan Xu, Sam Westrick +4
Recent advances in quantum architectures and computing have motivated the development of new optimizing compilers for quantum programs or circuits. Even though steady progress has…
DePa: Simple, Provably Efficient, and Practical Order Maintenance for Task Parallelism
Sam Westrick, Larry Wang, Umut A. Acar
A number of problems in parallel computing require reasoning about the dependency structure in parallel programs. For example, dynamic race detection relies on efficient "on-the-fl…
Parallel Batch-dynamic Trees via Change Propagation
Umut A. Acar, Daniel Anderson, Guy E. Blelloch +2
The dynamic trees problem is to maintain a forest subject to edge insertions and deletions while facilitating queries such as connectivity, path weights, and subtree weights. Dynam…
Hierarchical Memory Management for Mutable State
Adrien Guatto, Sam Westrick, Ram Raghunathan +2
It is well known that modern functional programming languages are naturally amenable to parallel programming. Achieving efficient parallelism using functional languages, however, r…