Research

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.