Programming Languages and Formal Verification
About Us
We work on designing and implementing programming language and formal verification tools and techniques that enable the development of high-assurance trustworthy software.
Graduate Researchers
Given name | Family name | Profile | Thesis Title |
---|
Zhuo | Chen | Profile | A Verified Cost Model for Call-By-Push-Value Lambda Calculus |
Louis | Cheung | Profile | Formally Verified Data Compression Algorithms |
Vincent | Jackson | Profile | Mechanised High-level Verification for Concurrent Low-level Programs |
Pilar Selene Linares | Arevalo | Profile | Composing Linear Types and Separation Logic Proofs of Memory Safety |
Mak | Nazecic-Andrlon | Profile | Efficient interval reasoning for floating-point arithmetic |
Pengbo | Yan | Profile | Proving Obliviousness with Formal Verification |