Applying mathematical methods to prove the correctness and security of systems, protocols, and software in critical environments.
Formal Verification is a research area focused on the use of logic-based techniques to rigorously verify the behavior of hardware, software, and cryptographic protocols. Unlike testing or simulation, formal methods aim to mathematically prove that a system adheres strictly to its specification, including its security properties. This includes verifying the absence of vulnerabilities such as buffer overflows, logic errors, or protocol flaws. In cybersecurity, formal verification is especially important for high-assurance systems, where failure or compromise could have severe consequences. Research in this area advances the development of provably secure systems, trusted computing bases, and reliable critical infrastructure.
Contact cyber@uq.edu.au for more information.
