Kasper Svendsen (original) (raw)

A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic

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

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

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

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

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

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

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

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

We present a new approach to admissibility for dependent type theories extended with partial types.

Verifying Generics and Delegates

We present a program logic for a subset of C# that includes generics and anonymous delegates with variable capture.

Design Patterns in Separation Logic

We present separation logic specifications for a number of classic design patterns including the subject-observer pattern, the flyweight pattern and the iterator pattern.