33 citations · 42 across the 9 of their papers we have counts for
15 papers
Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
Zachary Grannan, Aurea Bílá, Jonáš Fiala +4
Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability…
Formal Foundations for Translational Separation Logic Verifiers (extended version)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy +2
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3.…
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
Federico Poli, Xavier Denis, Peter Müller +1
Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not…
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau +2
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program a…
Resource Specifications for Resource-Manipulating Programs
Zachary Grannan, Alexander J. Summers
Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs…
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters
Aurea Bílá, Jonas Hansen, Peter Müller +1
Iteration is a programming operation that traditionally refers to visiting the elements of a data structure in sequence. However, modern programming systems such as Rust, Java, and…
REST: Integrating Term Rewriting with Program Verification (Extended Version)
Zachary Grannan, Niki Vazou, Eva Darulova +1
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables fl…
Formally Validating a Practical Verification Condition Generator (extended version)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself cor…
Rich Specifications for Ethereum Smart Contract Verification
Christian Bräm, Marco Eilers, Peter Müller +2
Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses,…
Local Reasoning for Global Graph Properties
Siddharth Krishna, Alexander J. Summers, Thomas Wies
Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expres…
Modular Verification of Heap Reachability Properties in Separation Logic
Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller
The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning…
Permission Inference for Array Programs
Jérôme Dohrau, Alexander J. Summers, Caterina Urban +2
Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this…
Automating Deductive Verification for Weak-Memory Programs
Alexander J. Summers, Peter Müller
Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logic…
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
Peter Müller, Malte Schwerhoff, Alexander J. Summers
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to…
The Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew J. Parkinson, Alexander J. Summers
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has rece…