37 citations · 133 across the 25 of their papers we have counts for
16 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…
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…
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti +1
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From…
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen +3
We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-or…
Logical Relations for Formally Verified Authenticated Data Structures
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are…
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva +1
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but the…
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program log…
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre +3
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational p…
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros +4
We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running…
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros +4
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the pro…
Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter +2
Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logi…
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti +2
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration,…
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter +2
Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational pr…