Model-checking quantum Markov chains: towards verification techniques for quantum cryptographic systems. This project will develop effective techniques and practical tools for verification of correctness, safety and reliability of quantum cryptographic protocols and communication systems. It will promote Australia's global standing in quantum computing research and provide frontier technology to industry and governments nationally and internationally.
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
Reasoning about, and stepwise development of, quantum programs: a predicate transformer semantics approach. The project will provide a framework to reason about, and stepwise develop, quantum programs by rigorous predicate transformer semantics, and generate breakthrough theory and frontier techniques for quantum software engineering.
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.