From the 2 of 4 linked papers with an AI index.
4 papers · 1 filter
Mizzle: A Complete Concurrent Incorrectness Logic for Preventing False Alarms in Agentic Bug Finding
Alexandre Moine, Sam Westrick, Joseph Tassarotti
The paper presents Mizzle, a mechanized concurrent incorrectness separation logic for OCaml that lets large language models attach machine‑checked proofs to bug reports, eliminatin…
A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, Joseph Tassarotti
The paper introduces Parcas, a concurrent separation logic that uses work and span credits to verify the parallel time complexity of fork‑join programs, and demonstrates its use on…
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…
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…