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.
.pdf
Reasoning About Monotonicity in Separation Logic
A. Timany and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
.pdf
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.
.pdf
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.
.pdf
Mechanized Logical Relations for Termination-Insensitive Noninterference
S.O. Gregersen, J. Bay, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
.pdf
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
[preprint] .pdf
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
D. Frumin, R. Krebbers, L. Birkedal
Submitted for publication.
[preprint] .pdf website Coq development
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
.pdf website Coq development
Compositional Non-Interference for Fine-Grained Concurrent Programs
D. Frumin, R. Krebbers, and L. Birkedal
In S&P 2021: Security and Privacy (Oakland)
[preprint] .pdf Coq development
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
.pdf technical appendix Coq development
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
.pdf
Mechanized Relational Verification of Concurrent Programs with Continuations
A. Timany and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
.pdf
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
.pdf
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
.pdf
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
.pdf
ReLoC: a Mechanised Relational Logic for Fine-Grained Concurrency
D. Frumin, R. Krebbers, and L. Birkedal
In LICS 2018: Logic in Computer Science
.pdf
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
.pdf
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
.pdf
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
.pdf
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
.pdf
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
.pdf technical appendix
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
.pdf
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
.pdf
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
.pdf
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
.pdf
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
.pdf
Interactive Proofs in Higher-Order Concurrent Separation Logic
R. Krebbers, A. Timany, and L. Birkedal
In POPL 2017: Principles of Programming Languages
.pdf
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
.pdf
Higher-Order Ghost State
R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer.
In ICFP 2016: International Conference on Functional Programming
.pdf
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
.pdf
A Kripke Logical Relation for Effect-Based Program Transformations
L. Birkedal, G. Jaber, F. Sieczkowski, and J. Thamsborg
Information and Computation, 2016
.pdf
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
.pdf
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
K. Svendsen, F. Sieczkowski, and L. Birkedal
In ESOP 2016: European Symposium on Programming
.pdf
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
.pdf
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
.pdf
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
.pdf
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
.pdf
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
.pdf
Step-indexed Logical Relations for Probability
A. Bizjak, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
.pdf
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
.pdf
A Separation Logic for Fictional Sequential Consistency
F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-Pharapod
In ESOP 2015: European Symposium on Programming
.pdf
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
.pdf
A Model of Countable Nondeterminism in Guarded Type Theory
A. Bizjak, L. Birkedal, and M. Miculan
In TLCA 2014: Typed Lambda Calculus and Applications
.pdf
Impredicative Concurrent Abstract Predicates
K. Svendsen and L. Birkedal
In ESOP 2014: European Symposium on Programming
.pdf
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.
.pdf
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
.pdf
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
.pdf
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
.pdf
Modular Reasoning about Separation of Concurrent Data Structures
K. Svendsen, L. Birkedal, and M. Parkinson
In ESOP 2013: European Symposium on Programming
.pdf
A Note on the Transitivity of Step-Indexed Logical Relations
Lars Birkedal and Ales Bizjak
Manuscript, 2012
.pdf
Logical Relations for Fine-Grained Concurrency
A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer
In POPL 2013: Principles of Programming Languages
.pdf
Views: Compositional Reasoning for Concurrency
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang
In POPL 2013: Principles of Programming Languages
.pdf
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.
.pdf
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.
.pdf
A Concurrent Logical Relation
L. Birkedal, F. Sieczkowski, and J. Thamsborg
In CSL 2012: Computer Science Logic
.pdf
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
.pdf
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,
.pdf
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.
.pdf
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.
.pdf
Fictional Separation Logic
J.B. Jensen and L. Birkedal
In ESOP 2012: European Symposium on Programming
.pdf
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
.pdf