Dr Peter Höfner is a Professor at the Australian National University (ANU), which he joined in February 2020. He regularly serves as Acting Head of the School of Computing. Before joining ANU, he worked for nearly a decade as a (Principal) Research Scientist at Data61, CSIRO (formerly NICTA). In parallel, he held concurrent appointments as Conjoint Associate Professor at the University of New South Wales (UNSW) and Honorary Senior Research Fellow at Macquarie University. Earlier in his career, he was a Postdoctoral Fellow at the University of Augsburg, Germany.
Research
Peter’s research vision is to fundamentally transform the way real-world software systems are built and engineered — ensuring their trustworthiness to the highest possible degree, backed by mathematical proof. He is a world leader in the formal analysis of network protocols used by emergency services and defence organisations worldwide. His team was the first to rigorously formalise the AODV routing protocol (standardised by the IETF and integrated into IEEE 802.11s), uncovering routing loops that contradicted popular belief and the official standard — findings that directly influenced the development of its successor, AODVv2.
As part of DARPA’s High-Assurance Cyber Military Systems (HACMS) programme, Peter led a team that designed and formally verified protocols subsequently deployed in operational unmanned aircraft built by Boeing. In 2023, DARPA honoured this work with its Game Changer Award, recognising its profound and lasting impact on national security. He currently leads a AUD$1 million project funded by Australia’s Defence Science and Technology Group, developing generic frameworks for verifying concurrent data structures used to protect sensitive infrastructure from cyber attacks.
To realise his research vision, Peter collaborates with leading researchers worldwide and with industry and government partners including Amazon Web Services, the Defence Science and Technology Group, DARPA, ProofCraft, and OpenBSD.
Education
As Associate Director of Education within the ANU School of Computing (2022–2026), Peter combined his scientific vision with a commitment to rigorous curriculum development and educational innovation. He led the design and transformation of curricula across eight computing programs and five diplomas, supporting over 6,000 student enrolments per semester — over 10% of ANU’s total student body. He was the academic lead for the Australian Computer Society (ACS) accreditation of ANU’s computing programs, critical for students’ visa eligibility and professional practice pathways.
Peter redesigned COMP3610/6361 Principles of Programming Languages and created the new course COMP4011/8011 Advanced Topics in Formal Methods and Programming Languages (2024), offering students cutting-edge knowledge at the intersection of software verification theory and practice. He also designed and launched a New Convenor Workshop for early-career academics, a model subsequently adopted across the College of Systems and Society.
Professional Leadership
Peter is the elected Vice Chair of the International Federation for Information Processing (IFIP) Technical Committee 2 — Software: Theory and Practice, an international body comprising 17 Working Groups and over 450 researchers and ICT professionals. He also serves as elected Chair of IFIP Working Group 2.1 on Algorithmic Languages and Calculi and as an elected member of IFIP Working Group 2.3 on Programming Methodology.
He serves on the editorial board of the Journal of Logical and Algebraic Methods in Programming (JLAMP) and on the steering committees of RAMiCS and MARS — the latter of which he founded in 2015. He is also a member of the Formal Methods Europe (FME) Industry Committee.
Key Areas of Expertise
- Formal Methods & Software Verification — developing mathematical proofs to guarantee software correctness
- Concurrency & Distributed Systems — verifying real-world concurrent and distributed software
- Protocol Security & High-Assurance Systems — analysing and improving protocols used in critical infrastructure
- Process & Program Algebras — algebraic foundations for reasoning about software behaviour