Verification and analysis of quantum programs. This project aims to develop theoretical foundations and techniques, as well as efficient algorithms and effective tools, for the verification and analysis of quantum programs. This project will introduce new ideas and techniques to tackle the problem of verifying and analysing quantum programs and provide efficient algorithms and effective tools to help quantum program compilation and optimisation. Successful development of the outcomes and tools i ....Verification and analysis of quantum programs. This project aims to develop theoretical foundations and techniques, as well as efficient algorithms and effective tools, for the verification and analysis of quantum programs. This project will introduce new ideas and techniques to tackle the problem of verifying and analysing quantum programs and provide efficient algorithms and effective tools to help quantum program compilation and optimisation. Successful development of the outcomes and tools in this project will help Australian industries build frontier technologies for quantum software engineering and establish and preserve their competitive status in the era of quantum computing.Read moreRead less
Symbolic synthesis of knowledge-based program implementations. Systems with concurrent streams of activity are ubiquitous in computer hardware and software designs, but are conceptually complex, and fraught with faults and inefficiency. The project aims to address these difficulties by automating aspects of system design, to relieve the designer of the need to reason about complex patterns of information flow.
Formal Verification of Quantum Logic Circuits. The project aims to develop comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits. The research is timely as the rapid growth of quantum computing hardware makes it an urgent task to develop verification techniques for quantum hardware design and quantum compilers. The successful development of the algorithms and software tools proposed in this project will significantly adva ....Formal Verification of Quantum Logic Circuits. The project aims to develop comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits. The research is timely as the rapid growth of quantum computing hardware makes it an urgent task to develop verification techniques for quantum hardware design and quantum compilers. The successful development of the algorithms and software tools proposed in this project will significantly advance the knowledge on formal verification of quantum circuits and help Australian quantum start-ups build and maintain an internationally leading position in the rapidly emerging quantum electronic design automation (EDA) industry.Read moreRead less
Coupling Techniques for Reasoning about Quantum Programs. Quantum software is indispensable for unleashing the super-power of quantum computing. This project aims to develop, for the first time, effective techniques for reasoning about the equivalence of quantum programs, with applications for verifying quantum compilers and quantum cryptographic protocols. The successful development of the outcomes and tools proposed in this project will significantly advance the knowledge on logical and mathem ....Coupling Techniques for Reasoning about Quantum Programs. Quantum software is indispensable for unleashing the super-power of quantum computing. This project aims to develop, for the first time, effective techniques for reasoning about the equivalence of quantum programs, with applications for verifying quantum compilers and quantum cryptographic protocols. The successful development of the outcomes and tools proposed in this project will significantly advance the knowledge on logical and mathematical foundations of quantum programming theory and thereby help Australian industries to build frontier technologies for quantum software engineering – in particular for quantum compilers – as well as establish and preserve their competitive status in the quantum computing era.Read moreRead less
Automation of metric temporal reasoning. A major contemporary engineering concern is to ensure the predictable and robust operation of computer systems involving software, hardware, and human users. The need for systematic and careful construction of such systems requires the development of formal methods based on a dense view of time rather than the traditional step-by-step models.
automated strategic reasoning. Formal methods are used to ensure robust correct behaviour in design and implementation of computer systems. Traditional models of computer operation involve a linear sequence of behaviour but today’s systems are complex interactions between many components including the environment of the system and human users. Thus analysis is done via a logical game between components where each is trying to meet its specified requirements regardless of what others do: formalis ....automated strategic reasoning. Formal methods are used to ensure robust correct behaviour in design and implementation of computer systems. Traditional models of computer operation involve a linear sequence of behaviour but today’s systems are complex interactions between many components including the environment of the system and human users. Thus analysis is done via a logical game between components where each is trying to meet its specified requirements regardless of what others do: formalisms include branching time and competing coalitions of agents. This project is to take early advantage of recent breakthroughs in automated logical reasoning with such models by the investigator to deliver general practical techniques of system development and verification.Read moreRead less
Verification of quantum cryptographic protocols: a process algebra approach. Security analysis of quantum cryptographic systems is notoriously difficult. This project aims to develop theoretic foundations and algorithms, as well as efficient software tools, to verify quantum cryptographic protocols by innovatively bridging two research fields: quantum cryptography and quantum process algebra. The pioneering research may provide innovative, game-changing security technologies for banks, business, ....Verification of quantum cryptographic protocols: a process algebra approach. Security analysis of quantum cryptographic systems is notoriously difficult. This project aims to develop theoretic foundations and algorithms, as well as efficient software tools, to verify quantum cryptographic protocols by innovatively bridging two research fields: quantum cryptography and quantum process algebra. The pioneering research may provide innovative, game-changing security technologies for banks, business, finance, security industry, police, and counter-terrorism both within Australia and globally.Read moreRead less
Assuring dependability of complex adaptive multi-agent systems using time bands. As the complexity of computer-based systems rapidly increases, we need new methods for assuring their correct behaviour. This project will provide a means of relating behaviour at different timescales, enabling us to understand how the long-term behaviour of a system results from the short-term interactions between its components.
Process algebra approach to distributed quantum computation and secure quantum communication. This project will develop effective methods for reasoning about the behaviours of distributed quantum computing and communicating systems. The developed methods will provide effective techniques for verifying security of quantum cryptographic protocols.
Relaxed correctness criteria for modern multi-core architectures. This project seeks to lay groundwork for fully exploiting the potential of multicore computers. Multicore computers have become ubiquitous over the last decade, now being standard in everything from laptops to mobile phones. Their benefits are clear – better performance leading to more sophisticated applications. Key to ensuring those benefits are complex, and often subtle, algorithms that exploit the parallelism that multicore co ....Relaxed correctness criteria for modern multi-core architectures. This project seeks to lay groundwork for fully exploiting the potential of multicore computers. Multicore computers have become ubiquitous over the last decade, now being standard in everything from laptops to mobile phones. Their benefits are clear – better performance leading to more sophisticated applications. Key to ensuring those benefits are complex, and often subtle, algorithms that exploit the parallelism that multicore computers offer. This project aims to lay foundations for extending those benefits to applications where high reliability is a concern. It plans to do so by developing theoretical results about the correctness of algorithms on standard multicore computers, and practical tools and techniques to help programmers of multicore computers to better understand the behaviour of their code.Read moreRead less