Current Research Projects
- Center for Basic Research in Program Verification (CPV).
- Iris: A Higher-Order Concurrent Separation Logic Framework, implemented and verified in the Coq proof assistant.
- Verification and Smart Contracts WP of Concordium Blockchain Research Center Aarhus (COBRA).
- DIGIT WP7: Blockchain.
- DIGIT WP8: Automated Verification and Synthesis.
- Troupe - a programming language for concurrent and distributed programming with dynamic information flow control.