Complexity in Algebra and Algebra in Complexity: the role of finite semigroups and general algebra. Algebra and logic form the mathematical framework for expressing and analysing algorithms and their difficulty. We can then scientifically analyse what makes some tasks more difficult than others. This project unifies parallel areas of algebra to focus on two key topics at this interface between algebra and computational complexity. As a flow on, our work can uncover new algorithms for solving ....Complexity in Algebra and Algebra in Complexity: the role of finite semigroups and general algebra. Algebra and logic form the mathematical framework for expressing and analysing algorithms and their difficulty. We can then scientifically analyse what makes some tasks more difficult than others. This project unifies parallel areas of algebra to focus on two key topics at this interface between algebra and computational complexity. As a flow on, our work can uncover new algorithms for solving constraint problems and for the study of formal languages.
With a team of top international researchers developing new interactions between mathematics and the study of algorithms, the project will foster a culture of innovation and bring Australia into the play in this internationally competitive area.Read moreRead less
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.
Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that woul ....Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that would benefit by such technology is the Australian Navy, which is increasingly being confronted with the challenge of integrating off-the-shelf components in large Naval Combat Systems. Read moreRead less
Parameterized Algorithm Design and Complexity Analysis: New Methods and Strategic Applications in the FPT Algorithmic Server Project. A fundamental discovery of the first decades of computer science is that completely efficient (polynomial time) algorithms probably do not exist for thousands of natural computational problems. The project will result in new methods for designing and analyzing algorithms for hard problems with natural parameters, and in improved
algorithms for these problems.
Approximate algorithms and architectures for area efficient system design. This project aims to develop simpler but reliable image recognition systems that can run on low-cost, small-scale platforms, for use in driver monitoring system (DMS) applications. Cheaper reliable DMS will lead to wider availability of this technology to end users and improve safety of motor vehicles. This project will develop approximate algorithmic and circuit techniques, provide training for research students and buil ....Approximate algorithms and architectures for area efficient system design. This project aims to develop simpler but reliable image recognition systems that can run on low-cost, small-scale platforms, for use in driver monitoring system (DMS) applications. Cheaper reliable DMS will lead to wider availability of this technology to end users and improve safety of motor vehicles. This project will develop approximate algorithmic and circuit techniques, provide training for research students and build capability in the area of approximate computing. It is also expected to lead to commercial products, licences and revenue, which will enable new job creation.
Read moreRead less
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