People

Over the years, Peter has supervised 15 PhD students as well as numerous Masters, Honours, and intern students. Currently supervising 14 researchers and research students.

Current

  • Vismaya Venkateshwara PhD  ·  Associate Supervisor
    Verification of Concurrent Programs with Rely-Guarantee
    Australian National University, Australia  ·  since 2026
  • Myria Sarvay Intern
    Open Bisimilarity for the π-Calculus with Mismatch in Isabelle
    Australian National University, Australia  ·  since 2026
  • Michael Ostapenko Honours
    Finding Attacks by Means of Predicate Transformers
    Australian National University, Australia  ·  since 2026
  • Long Feng Project
    Implementing Incorrectness Logic in Isabelle/HOL
    Australian National University, Australia  ·  since 2026
  • Yi Yao PhD  ·  Associate Supervisor
    An Algebraic Framework for Push-Down Automata and Turing Machines
    Australian National University, Australia  ·  since 2025
  • Hayley Pattons PhD  ·  Associate Supervisor
    Effects of programming languages on runtime design
    Australian National University, Australia  ·  since 2025
  • Xin Lu PhD  ·  Associate Supervisor
    Incorrectness Logic and Program Analysis
    Australian National University, Australia  ·  since 2025
  • Jack Stodart PhD  ·  Primary Supervisor and Chair
    Extending Automatic Software Verifiers with Interactive Proofs
    Australian National University, Australia  ·  since 2024
  • Eric Hall PhD  ·  Associate Supervisor
    Formal Verification of Error-Correcting Codes
    Australian National University, Australia  ·  since 2024
  • Alyssa Sha PhD  ·  Chair
    The Role of 'Forgetting' in Machine Learning and its Applications
    Australian National University, Australia  ·  since 2022
  • Tiange Liu PhD  ·  Associate Supervisor
    Open Bisimilarity for the π-Calculus
    Australian National University, Australia  ·  since 2022 -
  • Ryan Barry MPhil  ·  Primary Supervisor and Chair
    Proof Engineering for Linear Temporal Logic
    Australian National University, Australia  ·  since 2022
  • Weiyou Wang PhD
    Justness: Laying the foundations for verifying liveness properties
    Australian National University, Australia  ·  since 2020
  • Raja Oktovin Parhasian Damanik PhD  ·  Associate Supervisor
    Knowledge Problems in Security Protocols Through Term Rewriting
    Australian National University, Australia  ·  since 2020

PhD & MPhil Alumni

  • Callum Bannister PhD
    Forward with Separation Logic
    University of New South Wales, Australia  ·  January 2019
  • Ben Coughlan PhD  ·  Administrative Support
    Unmanned Aerial Vehicles, Energy Management, Control Systems
    Australian National University, Australia  ·  2010 - 2018
  • Insa Stucke PhD  ·  Associate Supervisor
    Verification of Relational Programs Supported by Theorem Provers
    Christian-Albrechts-Universität zu Kiel, Germany  ·  2012 - 2017
  • Han Hing Dang PhD  ·  Associate Supervisor
    Algebraic Calculi for Separation Logic
    University of Augsburg, Germany  ·  2009 - 2015

Postdoctoral Alumni

  • Roger Su
    Australian National University, Australia  ·  2022-2025
  • Ian Shillito
    Australian National University, Australia  ·  2022-2024

Other Alumni

  • Kevin Zhu Masters
    UX Design, Implementation and Evaluation for a Social Choice Board Game App
    Australian National University, Australia  ·  2026  [PDF]
  • Myria Sarvay Project
    Implementing π-Calculus with Mismatch in Isabelle/HOL based on Nominal Logic
    Australian National University, Australia  ·  2025
  • James Noonan Honours
    Conditional Valuation Algebras: Directionality and Efficient Inference
    Australian National University, Australia  ·  2025
  • Matthew Cawley Honours
    An IDE for the domain-specific language AWN
    Australian National University, Australia  ·  2025
  • Clint Del Borello Masters
    Algebraic Verification of Graph Algorithms using Isabelle/HOL
    Australian National University, Australia  ·  2025
  • Kaloosh Verrell Honours
    A Constraint-Solver-Based Board Game Voting System
    Australian National University, Australia  ·  2025
  • Pramo Samarasinghe Project
    Translating Timed Process Algebras into mCRL2
    Australian National University, Australia  ·  2024
  • Tianyuan Liu Honours
    HWMP Modeling by a Process Algebra for Wireless Mesh Networks
    Australian National University, Australia  ·  2023
  • Xiangyun Kong Masters
    User Data Analysis for a Video-Based App
    Australian National University, Australia  ·  2021
  • Anna Moscato Honours
    Applying Predicate Transformersfor Concurrency
    Australian National University, Australia  ·  2021
  • Callum Koh Honours
    Mechanising a Translation between Process Algebras in Isabelle/HOL
    Australian National University, Australia  ·  2021
  • Tina Ji Honours
    Partial Order Reduction for Protocols in Uppaal
    Australian National University, Australia  ·  2021
  • Ming Xu Masters
    Extended Labelled Transition Systems in Isabelle/HOL
    Australian National University, Australia  ·  2021
  • Pramo Samarasinghe Intern
    Translating Timed Process Algebras
    Australian National University, Australia  ·  2020-21
  • Cameron Pappas Intern
    Implementing and Analysing timed Routing Protocols in Isabelle/HOL
    Macquarie University, Australia  ·  2020
  • Aleksandar Miladinovic Intern
    Verifying Properties of the Routing Protocol OSPF
    Data61,CSIRO, Australia  ·  2020-21
  • Linda Kwan Intern
    Analysing Routing Attacks for OSPF in Uppaal
    Australian National University, Australia  ·  2020-21
  • Callum Koh Intern
    Formalising the Process Algebra mCRL2 in Isabelle/HOL
    Australian National University, Australia  ·  2020-21
  • Tina Ji Intern
    Optimising Models for Routing Protocols in Uppaal
    Data61,CSIRO, Australia  ·  2020-21
  • Courtney Darville Intern
    Attack Models for the OSPF Routing Protocol
    Data61,CSIRO and UNSW, Australia  ·  2020
  • Ranit Bose Intern
    Modelling Attacks for Routing Protocols
    Data61,CSIRO, Australia  ·  2020-21
  • Adam Pam Intern
    Modelling Routing Attacks in Uppaal
    Macquarie University, Australia  ·  2020
  • Weiyou Wang Masters
    Mechanising ACP in Isabelle/HOL
    University of New South Wales, Australia  ·  2019
  • Weiyou Wang Intern
    Modelling and Analysing the OSPF Routing Protocol
    University of New South Wales, Australia  ·  2019-2020
  • Ryan Barry Honours
    Formal Modelling and Analysis of OLSRv2
    University of New South Wales, Australia  ·  2019
  • Felix Pribyl Intern
    From AWN to CakeML
    University of Augsburg, Germany  ·  2019
  • Pierre Liorit Intern
    Analysing Link Layer Protocols
    École Polytechnique, France  ·  2019
  • Saya Lau Masters
    Test-Case Generation for Model-Checking Wireless Mesh Network
    University of New South Wales, Australia  ·  2019
  • Jack Drury Intern
    Modelling and Analysing the OSPF Routing Protocol
    University of New South Wales, Australia  ·  2019-20
  • Anran Wang Intern
    Expressiveness of Process Algebras with Broadcast Mechanisms
    University of Hamburg, Germany  ·  2018
  • Michael Markl Intern
    A Process Algebra for Link Layer Protocols
    University of Augsburg, Germany  ·  2018
  • Filippo De Bortoli Intern
    Verifying Liveness Properties of Distributed Systems
    University of Dresden, Germany  ·  2018
  • Ryan Barry Intern
    Formal Modelling of OLSRv2
    University of New South Wales, Australia  ·  2018
  • Djurre van der Wal Masters
    Model Checking a Process Algebra for Wireless Mesh Networks with a Formally Validated mCRL2 Back End
    University of Twente, Netherlands  ·  July 2018
  • Daniel Brownlow Intern
    Improving Automatic Translating AWN to Uppaal
    University of New South Wales, Australia  ·  2018/19
  • Katja Möhring Bachelor
    Automated Translation from the Process Algebra AWN to the Model Checker Uppaal
    University of Hamburg, Germany  ·  October 2017
  • Victor Dyseryn Intern
    Analysing Mutual Exclusion using Process Algebra with Signals
    École Polytechnique, France  ·  2017
  • Katja Möhring Intern
    Expressiveness in Slow Petri Nets
    University of Hamburg, Germany  ·  2015
  • Bertrand Bevillard Intern
    Analysis of Protocols for High-assurance Networks
    École Polytechnique, France  ·  2015
  • Emile Bres Intern
    Timed Process Algebras for Network Protocols
    École Polytechnique, France  ·  2014
  • Rafael Blecher Intern
    Implementing Secure Protocols for Quadcopters
    University of New South Wales, Australia  ·  2014/15
  • Mojgan Kamali Masters
    Modeling and Verifying the OLSR Protocol Using Uppaal
    University of Agder, Norway  ·  June 2014
  • Lina Gundelwein Intern
    Type-Checking for Algebra of Wireless (Mesh) Network
    University of Paderborn, Germany  ·  2013
  • Julian Nickerl Intern
    Automatic Transformation from AWN to Uppaal
    University of Ulm, Germany  ·  2013
  • Maryam Kamali Intern
    Formal Modelling of Network Topologies
    Åbo Akademi University, Finland  ·  2013
  • Patrick Lehner Intern
    Automatic Transformation from AWN to Uppaal
    University of Augsburg, Germany  ·  2012
  • Sarah Edenhofer Bachelor
    Formal Specification of the AODV Routing Protocol
    University of Augsburg, Germany  ·  March 2012  ·  in German
  • Markus Brenner Intern
    Computational Support for Routing Algebra
    University of Ulm, Germany  ·  2012
  • Rohan Jacob Rao Intern
    Rigour in Network Routing: an Algebraic Model
    University of New South Wales, Australia  ·  2012/13
  • Stephan Zeissler Masters
    Development of a Web-Application for ATP Systems
    Bonn-Rhein-Sieg University of Applied Sciences, Germany  ·  2010  ·  in German, co-supervision with Prof. Dr. M.E. Müller, Hochschule Bonn-Rhein-Sieg.
  • Markus Teufelhart Bachelor
    Automatic Normalisation of Algebraic Formulas
    University of Augsburg, Germany  ·  2010  ·  in German
  • Sven Mentl Masters
    Requirements in Feature Algebra
    University of Augsburg, Germany  ·  September 2010  ·  in German
  • Andreas Zelend Masters
    Formal Product Families for Abstract Machines
    University of Augsburg, Germany  ·  November 2010
  • Stephan Lindner Masters
    A Structured Compendium for Infinite Semirings.
    University of Augsburg, Germany  ·  2009  ·  in German
  • Han Hing Dang Masters
    Algebraic Aspects of Separations Logic
    University of Augsburg, Germany  ·  2009
  • Yanan Zhong Masters
    Development and Implementation of a Database for Proofs generated by Automated Theorem Provers
    University of Augsburg, Germany  ·  2009  ·  in German
  • Turki Hatam Bekr Masters
    Algebraic Analysis of Multi-Player-Games
    University of Augsburg, Germany  ·  2008  ·  in German