A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal
We present a relational model of an advanced type-and-effect system that validates advanced type-based equivalences, such as parallelization.
Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic
Mike Dodds, Suresh Jagannathan, Matthew Parkinson, Kasper Svendsen, Lars Birkedal
This paper examines the formal specification and verification of custom synchronisation constructs. Our target is a library of channels used in automated parallelization to enforce sequential behaviour between program statements.
Transfinite Step-indexing: Decoupling Concrete and Logical Steps
Kasper Svendsen, Filip Sieczkowski, Lars Birkedal
Step-indexing is a powerful technique for stratifying the construction of recursive models of advanced type systems and logics. Current techniques enforce a tight coupling between concrete steps and unfoldings of this underlying recursive equation. We show how to weaken this coupling using transfinite step-indexing.
A Separation Logic for Fictional Sequential Consistency
Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod
We present a program logic for a high-level programming language with a weak memory model that supports both low-level reasoning about racy code and high-level reasoning about well-behaved code.
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen,
Aaron Turon, Lars Birkedal, Derek Dreyer
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce—user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.
impredicative Concurrent Abstract Predicates
Kasper Svendsen, Lars Birkedal
We present a program logic for modular reasoning about safety properties of concurrent, higher-order, reentrant, imperative code.
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Library
Kasper Svendsen, Lars Birkedal, Matthew Parkinson
We formally specify and verify a lock-based implementation of the C# Joins library using our HOCAP logic.
Modular Reasoning about Separation of Concurrent Data Structures
Kasper Svendsen, Lars Birkedal, Matthew Parkinson
ESOP 2013
We present a spec. pattern for concurrent data structures that is independent of how clients intend to use instances of the data structure.
Partiality, State, and Dependent Types
Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski
TLCA 2011
We present a new approach to admissibility for dependent type theories extended with partial types.
Verifying Generics and Delegates
Kasper Svendsen, Lars Birkedal, Matthew Parkinson
ECOOP 2010
We present a program logic for a subset of C# that includes generics and anonymous delegates with variable capture.
Design Patterns in Separation Logic
Neel Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse
TLDI 2009
We present separation logic specifications for a number of classic design patterns including the subject-observer pattern, the flyweight pattern and the iterator pattern.