Max Planck Institute for Software Systems

RGSep under Release/Acquire Consistency

RGSep is a program logic for reasoning about the correctness of concurrent programs that combines rely-guarantee reasoning and separation logic. Although RGSep was initially developed for sequential consistency, we show that it is also sound under the much weaker release-acquire...

Constructive characterisations of the must -preorder for asynchrony

De Nicola and Hennessy's must -preorder is a liveness preserving refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q . Owing to the universal quantification over clients, this definition does not yield a practical proof...

Misquoted No More: Securely Extracting F* Programs with IO

Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into lar...