Research Highlights

Earlier in my career, I worked on using executable logical descriptions to produce software that is "correct by construction": Over a number of years I introduced, and helped develop, a leading approach to automated proof in temporal logics: As formal techniques can be used to provide a novel route to the automated, logical analysis (through model-checking) of autonomous decision-making software (in the form of agents), we produced one of the first formal agent verification systems: Work with increasingly realistic scenarios then led on to development of the first viable (and still leading) fully automated verification system for practical rational agent programs: It became clear that this work could have importance across autonomous systems engineering and so, in collaboration with engineers, my work has turned to analysing and developing practical autonomous systems, primarily across aerospace and robotics: The last of these is particularly important, having an impact on how certification for truly autonomous unmanned air systems might be achieved.

It is now clear not only that this underlying verification technology is relevant across very many different autonomous and robotic systems, but that such verification is essential if these systems are to be accepted by engineers, certified by regulators, and trusted by the public. Consequently, we promote this approach to verifiable autonomous systems

and are applying verification techniques across ethics, crowds, teamwork, human-robot interaction, and practical autonomous system verification: