1 citations · 2 across the 4 of their papers we have counts for
3 papers · 1 filter
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…