1 citations · 2 across the 4 of their papers we have counts for
4 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…
Refinement Proofs in Rust Using Ghost Locks
Aurea Bílá, João C. Pereira, Jan Schär +1
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementatio…
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…
Flexible Refinement Proofs in Separation Logic
Aurea Bílá, Christoph Matheja, Peter Müller
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementatio…