Ron van der Meyden
Professor
School of Computer Science and Engineering,
University of New South Wales
Sydney 2052,
Australia
email: last word of my name, at cse.unsw.edu.au
phone: +61 2 9385 6922
fax: +61 2 9385 5995
Office Location: K17 room 217G,
at grid reference K17 on the UNSW Kensington map.
Current Activities
Positions
No openings at present.
Potential Postgraduate Research Applicants
Please read this before contacting me with a supervision request.
Honors
Current Research Projects
- Can SAFE contracts be smart?, an extended case study in financial smart contracts.
- Lex Leinbniz, a declarative smart contract language designed for verifiability of correctness and security
- Fault Tolerant Autonomy, concerned with verification and synthesis of consensus protocols using the epistemic model checker MCK.
Publications
My Erdos number is 3, via:
- Tomasz Imielinski, Mario Szegedy, and
- Joseph Y. Halpern, Nathan Linial
Software
-
MCK a model checker for the logic of knowledge
Grants
- Australia's Economic Accelerator Grant: Development of a Commercial Version of a Software Model Checker, 2024/25.
- AFOSR/DST Australia Autonomy Initiative grant, 2020-2021: Verification and Synthesis of Fault-Tolerant Autonomous Systems (with J.Y. Halpern, Cornell)
- US Air Force, Asia Office of Aerospace Research and Development grant 2015/16:
Independence-based Optimization of Epistemic Model Checking
- ARC Discovery Grant 2012-2014, Symbolic synthesis of knowledge-based program implementations (with Kaile Su)
- ARC Discovery Grant 2010-2012, A formal foundation for security architecture (with Kai Engelhardt)
- US Air Force, Asia Office of Research and Development grant
2009/10: Security Protocol Optimization and Verification by Epistemic
Model Checking
- ARC Linkage grant 2008-2010: Model Checking Knowledge and Probability in Pursuit-Evasion Scenarios (with Defence R & D Canada)
- ARC Discovery Grant 2004-2007: Refinement of Temporal and Epistemic Specifications
in Asynchronous Systems (with Kai Engelhardt)
- ARC Discovery Grant 2001-2003: Model Checking Logics of Knowledge and Belief
- ARC Small Grant 2000: Compositional Abstraction for model
checking distributed systems designs using the logic of knowledge and
time. (with Kai Engelhardt)
- ARC Large Grant 2000-2002: Proof Theory for Extensions of
Temporal Logic (with Mark Reynolds, Murdoch).
- UTS Internal Research Grant, 1998: Logics of Belief for
Cryptographic Protocol Analysis
- ARC Large Grant 1997-1999: Knowledge-Based Programming of
Distributed Systems: From Specification to Implementation
- UTS Large Internal Research Grant 1996: Computational Analysis of
Knowledge Theory for Distributed Systems Design and Analysis
Research Centre Management Roles
As Chair (2001-2003) of the Research Committee, School of Computer Science and
Engineering, UNSW, I was a member of the teams (comprising multiple university,
government and industry partners) that constructed successful bids for and founded two major research centres:
- Smart Internet CRC, which was awarded $22M of Federal funding in 2001, matched by partner cash and kind contributions
to make up over $100M over 7 years. I was program leader of the CRC's Smart Personal Assistant
research program for the first year of operation of the centre.
- National ICT Australia, which
was awarded $129M of Federal funding for 2002-2006. I established and led the
NICTA Formal Methods program from NICTA's inception in 2002 to taking
sabbatical leave July 2006-July 2007. Significant outcomes from this program
include
- The formal verification of the seL4 microkernel, a joint project with the Embedded Real Time Operating Systems program and the Logic and Computation program.
- The Goanna static analysis tool, commercialised via a spinout Red Lizard Software, which was acquired by Synopsis.
All NICTA programs were closed in a NICTA reorganisation in 2007. NICTA merged with CSIRO's Digital Productivity business unit
to form Data61 in 2015.
I have also played a role in the Baker & McKenzie
Cyberspace Law and Policy Centre @ UNSW, a research centre in the Law School at UNSW,
as external representative on their management committee.
Invited/Keynote Addresses
- EASYHAT workshop on Evaluation of Adaptive Systems for
Human-Autonomy Teaming, IJCAI, Aug 2019, Macau.
- APAC Blockchain Conference, Sydney, July 2019 (panelist)
- Panelist, Australian Davos Committtee Blockchain Forum, Adelaide, March 2019. (panelist)
- CLIMA 2010, 11th Int. Workshop on Computational Logic in Multi-Agent Systems,
Lisbon, Aug 2010.
- DEON'02, Sixth International Workshop on
Deontic Logic in Computer Science, Imperial College, London, UK, May, 2002
- combined 10th international symposium on "Temporal Representation
and Reasoning" and 4th International Conference on Temporal Logic
(TIME-ICTL-2003), Cairns, Queensland, Australia July 8-10, 2003.
- Agentlink/Colognet Symposium on Logic-based Agent Verification, Liverpool, July 2004
- Workshop on Games and Knowledge, Liverpool, July 2004
- First Indian Conference on Logic and its relationship to other disciplines,
Mumbai, India, Jan 8-13, 2005.
Board Memberships
Program Committee Memberships & Editorial
Current:
Past PC memberships
Education
UNSW Courses taught
Summer School Courses
Research Students, Postdocs
- Godfrey Wong - Knowledge in Consensus Protocols
- Vir Nath Pathak (co-supervisor) - Post-Quantum Cryptography
Former Students, Postdocs
- Xiaowei Huang, postdoc (now at Liverpool University)
- Stephen Chong, postdoc (now at Harvard)
- Omar I. Al Bataineh, Masters by research (now at Nanyang Technological University)
- Chenyi Zhang, PhD & Postdoc (now at Jinan University, China)
- Manas K. Patra, Phd (now at Central University of Rajasthan)
- Peng Gao, Masters by Research
- Kai Engelhardt, Postdoc (now at Cog Systems)
- Kaile Su, Postdoc (now at Griffith University)
- Kai Baukus, Postdoc (now at BMW)
- Umberto Bonollo, (Ph.D. student, University of Melbourne, cosupervisor with Liz
Sonenberg)