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

Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion
Daniele Palombi, Jonathan Sterling
In MFPS 2022: Mathematical Foundations of Programming Semantics
.pdf
Sheaf semantics of termination-insensitive noninterference
Jonathan Sterling, Robert Harper
In FSCD 2022: Formal Structures for Computation and Deduction
.pdf
A stratified approach to Löb induction
Daniel Gratzer, Lars Birkedal
In FSCD 2022: Formal Structures for Computation and Deduction
.pdf
Normalization for multimodal type theory
Daniel Gratzer
In LICS 2022: Logic in Computer Science
.pdf
A Cubical Language for Bishop Sets
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
Logical Methods in Computer Science 2022
.pdf
Modalities and Parametric Adjoints
Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, Lars Birkedal
Transactions on Computational Logic 2022
.pdf
A Cost-Aware Logical Framework
Y. Niu, J. Sterling, H. Grodin, R. Harper
In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages
.pdf
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
S. F. Vindum, D. Frumin, L. Birkedal
In CPP 2022: ACM SIGPLAN International Conference on Certified Proofs and Programs
.pdf
Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines.
T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedal, and D. Devriese.
In CSF 2022: Computer Security Foundations
.pdf
Higher-order probabilistic adversarial computations: categorical semantics and program logics
A. Aguirre, G. Barthe, M. Gaboardi, D. Garg, S. Katsumata, and T. Sato
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
.pdf
Theorems for Free from Separation Logic Specifications
L. Birkedal, T. Dinsdale-Young, A. Gueneau, G. Jaber, K. Svendsen and N. Tzevelekos
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
.pdf
Client-Server Sessions in Linear Logic
Zesen Qian, G. A. Kavvos and Lars Birkedal
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
.pdf
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
In LMCS 2021: Logical Methods in Computer Science 17:3
.pdf
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
In PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
.pdf
Toward Complete Stack Safety for Capability Machines
Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal
In PRISC 2021: Principles of Secure Compilation
[abstract] .pdf
Cap’ ou pas cap’? Preuve de programmes pour une machine a capacites en presence de code inconnu
Aïna L. Georges, Armaël Gueneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
In JFLA 2021: Journees Francophones des Langages Applicatifs
.pdf
Reasoning About Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
In CPP 2021: ACM SIGPLAN International Conference on Certified Proofs and Programs
.pdf
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon F. Vindum and Lars Birkedal
In CPP 2021: Certified Proofs and Programs
.pdf
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
.pdf
Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese.
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
.pdf
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna L. Georges, Armaël Gueneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
.pdf
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
.pdf Coq development
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
In JFP 2021: Journal of Functional Programming
.pdf
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Dan Frumin, Robbert Krebbers, Lars Birkedal
In LMCS 2021: Logical Methods in Computer Science 17:3
.pdf
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
In ICFP 2020: ACM SIGPLAN International Conference on Functional Programming
.pdf website
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
In S&P 2021: Security and Privacy (Oakland)
.pdf Coq development
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
In LICS 2020: Logic in Computer Science
.pdf
Dual-Context Calculi for Modal Logic
G. A. Kavvos
In LMCS 2020: Logical Methods in Computer Science
.pdf
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
.pdf technical appendix Coq development
Mechanized Reasoning about a Capability Machine
Aïna Linn Georges, Alix Trieu, Lars Birkedal
In PRISC 2020: Principles of Secure Compilation
[abstract] .pdf
Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
In FSCD 2019: Formal Structures for Computation and Deduction,
.pdf
Implementing a Modal Dependent Type Theory
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
.pdf
Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany and Lars Birkedal
In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
.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
.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
.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

Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic
A. Timany, S. O. Gregersen, L. Stefanesco, L. Gondelman, A. Nieto, L. Birkedal
Submitted for publication
[preprint] pdf
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal
Submitted for publication
[preprint] pdf
Syntactic categories for dependent type theory: sketching and adequacy
Daniel Gratzer, Jonathan Sterling
[preprint] pdf