From the 6 of 19 linked papers with an AI index.
1 citations · 1 across the 7 of their papers we have counts for
19 papers
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter +2
The paper presents Elton, a higher-order separation logic for reasoning about probabilistic programs that may contain unknown adversarial code, introducing urn resources and delaye…
Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
The paper presents a method for constructing extensible program logics using effect handlers, enabling modular reasoning about effects such as concurrency, distributed execution, a…
Verifying Probabilistic Programs in Rust
Alexander Y. Bai, Joseph Tassarotti
The paper introduces Alerus, a framework that extends the Verus verification tool to support formal verification of probabilistic programs written in Rust using a lightweight encod…
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…
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
The paper proves that any linearizable concurrent data structure can be given a logically atomic specification in the Iris separation logic, and demonstrates this by mechanizing pr…