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

Christine Rizkallah

Christine Rizkallah

    Staff Members

    Given Name Family NameProfileEmail
    Aaron BembenekProfileaaron.bembenek@unimelb.edu.au
    CezaryKaliszykProfilecezary.kaliszyk@unimelb.edu.au
    Christine RizkallahProfilechristine.rizkallah.unimelb@gmail.com
    EllieRipley  (Honorary)Profileripley@negation.rocks
    IanShillitoProfileian.shillito@unimelb.edu.au
    LouisCheungProfilelouis.cheung@unimelb.edu.au
    Peter SchachteProfileschachte@unimelb.edu.au
    Pilar SeleneLinares ArevaloProfilepilarselene.linaresarevalo@unimelb.edu.au
    Toby MurrayProfiletoby.murray@unimelb.edu.au

    Graduate Researchers

    Given NameFamily NameProfilePrimary SupervisorCo-Supervisor(s)Thesis Title
    JeremyLindsayProfileCezary KaliszykChristine RizkallahProof Metrics in Formalised Mathematics
    PengboYanProfileOlya OhrimenkoRobert Sison, Thuan PhamProving Obliviousness with Formal Verification
    XingLiProfileChristine RizkallahPeter SchachteCost Semantics for Lazy Functional Programs
    Zoe O.ElwynTBDChristine RizkallahAbel Armas CervantesFormalising Quantitative Properties of Concurrent Processes

    Alumni

    Given Name Family NameProfilePrimary SupervisorCo-Supervisor(s) Thesis Title
    VincentJacksonProfileChristine RizkallahToby MurrayMechanised High-level Verification for Concurrent Low-level Programs
    Pilar SeleneLinares ArevaloProfileChristine RizkallahPeter SchachteComposing Linear Types and Separation Logic Proofs of Memory Safety
    Zhuo (Zoey)ChenProfileChristine RizkallahJohannes Åman Pohjola (external)A Verified Cost Model for Call-By-Push-Value Lambda Calculus
    LouisCheungProfileChristine RizkallahAlistair MoffatFormally Verified Indexed Pattern Search
    Mak Nazecic-AndrlonProfileHarald SondergaardPeter Schachte, Peter StuckeyEfficient Interval Reasoning for Floating-Point Arithmetic

    Projects

    Weekly Activities