Center for Basic Research in Program Verification

Department of Computer Science, Aarhus University


About

Software systems are an integral part of modern society, and software errors and security breaches pose enormous costs and risks. Center for Basic Research in Program Verification develops fundamental mathematically based models and logics for rigorous mathematical reasoning about correctness and security of software systems.

To read more about the research center go to the official center website.

Publications

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
In ESOP 2020: European Symposium on Programming, Dublin, Ireland
.pdf technical appendix Coq development
Mechanized Reasoning about a Capability Machine
Aïna Linn Georges, Alix Trieue, Lars Birkedal
In PRISC 2020: Principles of Secure Compilation, New Orleans, Louisiana, United States
[abstract] .pdf
Implementing a Modal Dependent Type Theory
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
.pdf
Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany and Lars Birkedal
In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming, Berlin, Germany
.pdf
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Møgelberg, Andrew M. Pitts, Bas Spitters
In MSCS 2019: Mathematical Structures in Computer Science
.pdf
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages, Lisbon, Portugal
.pdf
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages, Lisbon, Portugal
.pdf
Guarded Cubical Type Theory
Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans B. Grathwohl, Bas Spitters, Andrea Vezzosi
In JAR 2019: Journal of Automated Reasoning
.pdf
Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
In TOPLAS 2019: ACM Transactions on Programming Languages and Systems
.pdf

Draft papers

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
Submitted for publication
[preprint] .pdf
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
Submitted for publication
[preprint] .pdf
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
Submitted for publication
[preprint] .pdf Coq development