37 citations · 133 across the 25 of their papers we have counts for
9 papers · 1 filter
Iris in Lean
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu +9
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-…
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter +2
Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbit…
Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, dev…
Verifying Probabilistic Programs in Rust
Alexander Y. Bai, Joseph Tassarotti
Recent work has developed many techniques for formally verifying probabilistic programs. However, existing verification frameworks for probabilistic programs are restricted to idea…
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…
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their…
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Markus de Medeiros, Puming Liu, Kwing Hei Li +3
Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be diffic…
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen +3
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially…