Kasper Svendsen
Postdoctoral Researcher
ksvendsen@cs.au.dk
Dept. of Computer Science, Aarhus University
Turing 215, Aabogade 34, 8000 Aarhus C, Denmark
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.