Every engineering discipline needs mathematical foundations in order to have confidence in the behaviour of the artifacts that it produces. Logic and discrete mathematics provide that foundation for much of computer science.
Logic has a tradition going back at least to the ancient Greeks, but the field really exploded in relevance in the 20th century. Mathematical logicians like Godel and Turing laid down the fundamental theory about what computers can do, but also what they cannot do. Today, computer science is a key driver for research in logic: there are more logicians in computer science departments than in mathematics and philosophy departments
We are still not very good at engineering computational systems so that they have mathematical foundations that are as strong as in other engineering areas. There is an ongoing need to improve our capability in this area.
As the scope of application of computational systems broadens to encompass systems that operate in the real world (e.g., robots, cars) and in society (e-commerce, crypto-currency), or are built using multiple computers (the internet, multi-processor hardware, and distributed systems), there is a need for novel logical theory that builds in additional mathematical dimensions, such as probability theory, continuous mathematics, economic game theory, concurrency, security, and theories of information flow.
The Formal Methods Group works to develop these theoretical foundations for reasoning about computational systems, and for enabling computers themselves to perform such reasoning. The work results in logical theories and computational tools that enable the development of computational systems in a way that provides high degrees of assurance about their correctness, safety and security.
Dr. Paul Hunter studies mathematical games used in formal verification and graph theory. In particular, looking at using such games to explore the limit of what is and is not possible in automated verification. Paul's other research areas include investigating the expressiveness of temporal logics and, more recently, the incorporation of interactive tools and games to assist with teaching abstract concepts and alleviating mathematical anxiety.
Dr Eric Martin studies logical foundations to unify modes of reasoning beyond deduction, such as induction. The work encompasses applications to logic programming, modal logic and connections to formal learning theory and topological hierarchies. A current project is investigating a very general kind of sequent calculus for infinitary languages and inference rules, in a framework for contextual reasoning designed to, in particular, differentiate between sets and proper classes in a new way at the object level.
Prof. Ron van der Meyden works on the logical foundations for distributed computing and computer security. An outcome from a long program of research on this topic is MCK: a software system that reasons automaticaly about information flow in distributed and multi-agent systems. Ron's focus at present is on applications of logic to smart contracts and the distributed systems protocols that underpin blockchain and cryptocurrency systems.
Prof Carroll Morgan works on the design and implementation of logics/methods/practices for reasoning about correct programs (and how to make them): standard imperative programming, probabilisitic programs, and (supposed-to-be) secure programs. He is currently working a basic re-evaluation of what "privacy" and "security" actually (should) mean, and --once that is settled-- how to achieve them. Specifically, current work deals with tradeoffs between (differential) privacy and utility in an information-gathering exercise, and on how a machine learning algorithm can publish its conclusions without compromising the privacy of the particular data it is analysing or which was used for training.
Dr. Sebastian Sequoiah-Grayson is a senior lecturer in epistemics. He works across knowledge representation and reasoning, with particular interest in substructural epistemic logics and negative information.
Prof. Rob van Glabbeek works on mathematical models and formal languages for the representation of distributed systems and the verification of statements about them; in particular foundational work investigating the possibilities of such models and languages. Rob's recent focus is on the formalisation of liveness properties, expressing that goal states of distributed systems will be reached, and the fairness assumptions that need to be made in such formalisations.
A/Prof. Ralf Huuck works on application cyber security, aiming at ensuring that software is free from vulnerabilities that provide attack vectors to threat actors, particularly by means of automated methods. He is developing new foundations and methods for vulnerability detection by combining formal methods, AI and programming language techniques. He is currently collaborating with Fortune 500 companies to investigate application security needs and providing guidance on security implementation.