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.

    Staff

    Given name Family namePositionProfileEmail
    Aaron BembenekResearch FellowProfileaaron.bembenek@unimelb.edu.au
    Toby MurrayAssociate ProfessorProfiletoby.murray@unimelb.edu.au
    Christine RizkallahLecturerProfilechristine.rizkallah@unimelb.edu.au
    Peter SchachteLecturerProfileschachte@unimelb.edu.au

    Graduate Researchers

    Given name Family nameProfile Thesis Title
    ZhuoChenProfileA Verified Cost Model for Call-By-Push-Value Lambda Calculus
    LouisCheungProfileFormally Verified Data Compression Algorithms
    VincentJacksonProfileMechanised High-level Verification for Concurrent Low-level Programs
    Pilar Selene LinaresArevaloProfileComposing Linear Types and Separation Logic Proofs of Memory Safety
    Mak Nazecic-AndrlonProfileEfficient interval reasoning for floating-point arithmetic
    PengboYanProfileProving Obliviousness with Formal Verification

    Projects

    Automated Rely-Guarantee Generation
    The Cogent Project
    The COVERN Project
    The CATCH Project
    The Dargent Project
    The Wybe Project

    Weekly Activities

    Programming Languages and Verification Reading Group