Synthesis of Heap-Manipulating Programs from Separation Logic

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Hoare Type Theory

The VerCors verification toolset for verifying parallel and concurrent software

Program logic for developing and verifying distributed systems

Partial Commutative Monoids

Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

Probabilistic separation logics for verifying higher-order probabilistic programs.

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Test input generation using separation logic

An automated deductive program verifier based on concurrent separation logic

A Symbolic Executor based on Separaton Logic

Separation logic library for Coq

Coq tactics for certification of the results of SSL-based program synthesis via Hoare Type Theory.

Mostly Automated Proof Repair for Verified Libraries

An implementation of separation logic in Coq

Demos for lecture on Separation Logic by O'Hearn from CACM 2019.

Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol

Decision procedure for strong-separation logic

Verifying FF-A hypercalls using VMSL.