Programming Languages and Formal Verification

About Us

The Programming Languages and Formal Verification Group focuses on designing and implementing programming language and formal verification tools and techniques that ease the development of trustworthy software. By uniting formalised mathematical foundations and foundational language techniques with practical proof engineering, this research group investigates how to formally verifying that critical software components meet their specifications. Our work in this area ranges from foundational semantics and type systems techniques to industrial-strength verification tools, certified APIs, and certifying compilers for formally verifying the correctness of mathematical foundations, algorithms, systems software, and language runtime.

Theme Lead

Profile picture of Christine Rizkallah

Dr Christine Rizkallah

Senior Lecturer In Software Engineering
christine.rizkallah@unimelb.edu.au

    Staff Members

    Given Name Family NameProfileEmail
    Aaron BembenekProfileaaron.bembenek@unimelb.edu.au
    CezaryKaliszykProfilecezary.kaliszyk@unimelb.edu.au
    Christine RizkallahProfilechristine.rizkallah@unimelb.edu.au
    EllieRipley  (Honorary)Profileripley@negation.rocks
    Peter SchachteProfileschachte@unimelb.edu.au
    Toby MurrayProfiletoby.murray@unimelb.edu.au

    Graduate Researchers

    Given NameFamily NameProfilePrimary SupervisorCo-Supervisor(s)Thesis Title
    JeremyLindsayTBDCezary KaliszykChristine RizkallahProof Metrics in Formalised Mathematics
    PengboYanProfileOlya OhrimenkoRobert Sison, Thuan PhamProving Obliviousness with Formal Verification
    Pilar Selene Linares ArevaloProfileChristine RizkallahPeter SchachteComposing Linear Types and Separation Logic Proofs of Memory Safety
    VincentJacksonProfileChristine RizkallahToby MurrayMechanised High-level Verification for Concurrent Low-level Programs
    XingLiProfileChristine RizkallahPeter SchachteCost Semantics for Lazy Functional Programs
    Zoe O.ElwynTBDChristine RizkallahAbel Armas CervantesFormalising Quantitative Properties of Concurrent Processes
    Zhuo (Zoey)ChenProfileChristine RizkallahJohannes Åman Pohjola (external)A Verified Cost Model for Call-By-Push-Value Lambda Calculus

    Alumni

    Given Name Family NameProfilePrimary SupervisorCo-Supervisor(s) Thesis Title
    LouisCheungProfileChristine RizkallahAlistair MoffatFormally Verified Indexed Pattern Search
    Mak Nazecic-AndrlonProfileHarald SondergaardPeter Schachte, Peter StuckeyEfficient Interval Reasoning for Floating-Point Arithmetic

    Projects

    Weekly Activities