26 citations · 57 across the 11 of their papers we have counts for
16 papers
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…
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
Linard Arquint, Felix A. Wolf, Joseph Lallemand +5
We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and…
A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
Linard Arquint, Malte Schwerhoff, Vaibhav Mehta +1
Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, im…
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…
Sound Automation of Magic Wands (extended version)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks +2
The magic wand (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance…
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…