Modular Reasoning about Concurrent Higher-Order Imperative Programs (ModuRes)

ModuRes_logo

Over the last five years, mainstream programming languages such as Java, C#, and Scala have evolved to permit a powerful combination of language features: (a) mutable shared data structures, (b) higher-order functions, and (c) concurrency. These features are all very important for programming in practice. However, the combination of them makes it difficult to write correct and secure programs, and it is therefore very important to develop mathematically-based techniques for formal reasoning about correctness and security of programs with these features.

To get scalable methods that apply to realistic programs, it is crucial that the mathematical models and logics support modular reasoning, meaning that specifications and proofs can concentrate on the resources that a program actually acts upon, instead of its entire state.

The advent of separation logic has made it easier to reason modularly about first-order programs with shared mutable data (feature a). Building on the initial work on separation logic and on relational models for reasoning about program equivalence, there has recently been progress on (1) models and logics for modular reasoning about sequential imperative programs with higher-order functions (features a, b), and (2) models and logics for modular reasoning about low-level concurrent imperative programs (features a, c).

The ModuRes project will break new ground by developing mathematical models and logics for modular reasoning about programs written in realistic programming languages with all the challenging features (a, b, c). The project will lay the foundation for future software tools, which will be used to improve software practice.

The project will be led by Professor Lars Birkedal at Aarhus University, and will involve international collaboration with the PI's exceptionally strong network of international collaborators. The ModuRes project starts in the summer of 2013 and will run for five years. It is generously funded by an Advanced Sapere Aude Grant from the Danish Council for Independent Research for the Natural Sciences (FNU).

We are looking for PhD students and postdocs. Please email Lars Birkedal for information.

Postdocs and PhD students at Aarhus

Former Postdocs and PhD students at Aarhus

Iris Project

Tutorial Material

Selected Related Publications:

Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
S.F. Vindum and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
Reasoning About Monotonicity in Separation Logic
A. Timany and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
L. Gondelman, S.O. Gregersen, A. Nieto, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, S. Huyghebaert, D. Devriese, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
Mechanized Logical Relations for Termination-Insensitive Noninterference
S.O. Gregersen, J. Bay, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
L. Skorstengaard, D. Devriese, and L. Birkedal
Extended version of POPL 2019 paper. Submitted for publication
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
D. Frumin, R. Krebbers, L. Birkedal
Submitted for publication.
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
P.G. Giarrusso, L. Stefanesco, A. Timany, L. Birkedal, R. Krebbers
In ICFP 2020: International Conference on Functional Programming
Compositional Non-Interference for Fine-Grained Concurrent Programs
D. Frumin, R. Krebbers, and L. Birkedal
In S&P 2021: Security and Privacy (Oakland)
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
M. Krogh-Jespersen, A. Timany, M.E. Ohlenbusch, S.O. Gregersen, and L. Birkedal
In ESOP 2020: European Symposium on Programming, Dublin, Ireland
Mechanized Reasoning about a Capability Machine
A.L. Georges, A. Trieue, and L. Birkedal
Extended Abstract for talk at PRISC 2020: Principles of Secure Compilation
Mechanized Relational Verification of Concurrent Programs with Continuations
A. Timany and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal
In POPL 2019: Principles of Programming Languages
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
L. Skorstengaard, D. Devriese, and L. Birkedal
In POPL 2019: Principles of Programming Languages
Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management
L. Skorstengaard, D. Devriese, and L. Birkedal
ACM Transactions on Programming Languages (TOPLAS): 5, 2019
ReLoC: a Mechanised Relational Logic for Fine-Grained Concurrency
D. Frumin, R. Krebbers, and L. Birkedal
In LICS 2018: Logic in Computer Science
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic
R. Jung, R. Krebbers, J-H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer
Journal of Functional Programming, 28, 2018
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
Compositional Non-Interference for Concurrent Programs via Separation and Framing
A. Karbyshev, K. Svendsen, A. Askarov, and L. Birkedal
In POST 2018: Principles of Security and Trust
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
A. Aguirre, G. Barthe, L. Birkedal, A. Bizjak, M. Gaboardi, and D. Garg
In ESOP 2018: European Symposium on Programming
Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without OS support)
L. Skorstengaard, D. Devriese, and L. Birkedal
In ESOP 2018: European Symposium on Programming
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
A. Timany, L. Stefanesco, M. Krogh-Jespersen, and L. Birkedal
In POPL 2018: Principles of Programming Languages
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
The Essence of Higher-Order Concurrent Separation Logic
R. Krebbers, R. Jung, A. Bizjak, J.-H. Jourdan, D. Dreyer, and L. Birkedal
In ESOP 2017: European Symposium on Programming
Caper: Automatic Verification for Fine-Grained Concurrency
T. Dinsdale-Young, P. Pinto, K.J. Andersen, and L. Birkedal
In ESOP 2017: European Symposium on Programming
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
M. Krogh-Jespersen, K. Svendsen, and L. Birkedal
In POPL 2017: Principles of Programming Languages
Interactive Proofs in Higher-Order Concurrent Separation Logic
R. Krebbers, A. Timany, and L. Birkedal
In POPL 2017: Principles of Programming Languages
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi
In CSL 2016: Computer Science Logic
Higher-Order Ghost State
R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer.
In ICFP 2016: International Conference on Functional Programming
The Guarded Lambda Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
Logical Methods in Computer Science, 2016.
Journal version of FOSSACS 2015 paper
A Kripke Logical Relation for Effect-Based Program Transformations
L. Birkedal, G. Jaber, F. Sieczkowski, and J. Thamsborg
Information and Computation, 2016
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
K. Svendsen, F. Sieczkowski, and L. Birkedal
In ESOP 2016: European Symposium on Programming
Guarded Dependent Type Theory with Coinductive Types
A. Bizjak, H.B. Grathwohl, R. Clouston, R.E. Møgelberg, and L. Birkedal
In FOSSACS 2016: Foundations of Software Science and Computation Structures
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
D. Devriese, F. Piessens, and L. Birkedal
In EuroS&P 2016: European Symposium on Security and Privacy
Verifying Custom Synchronisation Constructs using Higher-Order Separation Logic
M. Dodds, S. Jagannathan, M.J. Parkinson, K. Svendsen, and L. Birkedal
ACM Transactions on Programming Languages and Systems (TOPLAS), 38(2:4), 2016
A Model of PCF in Guarded Type Theory
M. Paviotti, R.E. Møgelberg, and L. Birkedal
In MFPS 2015: Mathematical Foundations of Programming Semantics
ModuRes: a Coq library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages
F. Sieczkowski, A. Bizjak, and L. Birkedal
In ITP 2015: International Conference on Theorem Proving
Step-indexed Logical Relations for Probability
A. Bizjak, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
A Separation Logic for Fictional Sequential Consistency
F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-Pharapod
In ESOP 2015: European Symposium on Programming
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer
In POPL 2015: Principles of Programming Languages
A Model of Countable Nondeterminism in Guarded Type Theory
A. Bizjak, L. Birkedal, and M. Miculan
In TLCA 2014: Typed Lambda Calculus and Applications
Impredicative Concurrent Abstract Predicates
K. Svendsen and L. Birkedal
In ESOP 2014: European Symposium on Programming
Step-Indexed Relational Reasoning for Countable Nondeterminism
L. Birkedal, A. Bizjak, and J. Schwinghammer
Logical Methods in Computer Science, 9(4):1–23, October 2013.
Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency
A. Turon, D. Dreyer, and L. Birkedal
In ICFP 2013: International Conference on Functional Programming
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
L. Birkedal and R.E. Møgelberg
In LICS 2013: Logic in Computer Science
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
K. Svendsen, L. Birkedal, and M. Parkinson
In ECOOP 2013: European Conference on Object-Oriented Programming
Modular Reasoning about Separation of Concurrent Data Structures
K. Svendsen, L. Birkedal, and M. Parkinson
In ESOP 2013: European Symposium on Programming
A Note on the Transitivity of Step-Indexed Logical Relations
Lars Birkedal and Ales Bizjak
Manuscript, 2012
Logical Relations for Fine-Grained Concurrency
A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer
In POPL 2013: Principles of Programming Languages
Views: Compositional Reasoning for Concurrency
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang
In POPL 2013: Principles of Programming Languages
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
L. Birkedal, R. Møgelberg, J. Schwinghammer, and K. Støvring
Logical Methods in Computer Science, 8(4), October 2012.
Two for the Price of One: Lifting Separation Logic Assertions
J. Thamsborg, L. Birkedal, and H. Yang
Logical Methods in Computer Science, 8(3), September 2012.
A Concurrent Logical Relation
L. Birkedal, F. Sieczkowski, and J. Thamsborg
In CSL 2012: Computer Science Logic
Charge! a Framework for Higher-Order Separation Logic in Coq
J. Bengtson, J.B. Jensen, and L. Birkedal
In ITP 2012: International Conference on Theorem Proving
A Relational Realizability Model for Higher-Order Stateful ADTs
L. Birkedal, K. Støvring, and J. Thamsborg
Journal of Logic and Algebraic Programming, 81(4):491–521,
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning
D. Dreyer, G. Neis, and L. Birkedal
Journal of Functional Programming, February 2012.
A Step-Indexed Kripke Model of Hidden State
J. Schwinghammer, L. Birkedal, F. Pottier, B. Reus, K. Støvring, and H. Yang
Mathematical Structures in Computer Science, 2012.
Fictional Separation Logic
J.B. Jensen and L. Birkedal
In ESOP 2012: European Symposium on Programming
Formalized Verification of Snapshotable Trees: Separation and Sharing
H. Mehnert, F. Sieczkowski, L. Birkedal, and P. Sestoft
In VSTTE 2012: Verifiec Software, Theories, Toools, and Experiments