You are here

This technology has just been licensed

Improving computer security

Invention Number: 
A valuable invention for better computer security


For more than a decade, UNSW has been developing methods and software to verify whether hardware or software systems meet given specifications.  It checks the logic of the system to make sure it is correct.  Has the software programmer implemented what they intended? 

MCK (Model Checking Knowledge) is a novel model checker that supports several different ways of defining knowledge given a description of a multi-agent system and the observations made by the agents. 

Although model checking can be used in a variety of applications, it is especially valuable for verifying software and hardware security.

Features and Benefits 

•    Determine if system is making optimal use of information

•    Supports a range of knowledge semantics and choices of temporal language

•    First system to extend capability to agent knowledge

•    Used to analyse multi-agent systems with respect to properties stated in formal logic of knowledge, time and probability

Potential Applications

  • Software verification

  • Hardware security verification 

  • Decision support tool 

Technical Data 

Technical details and papers on MCK, epistemic model checking, and algorithms for epistemic logic are available here. 

The Opportunity 

UNSW is seeking a partner to work with the researchers on further developing this technology for additional applications.

Researcher Details

Professor Ron van der Meyden