Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap ....Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap between the informal requirements and the starting point of formally verifiable development. To minimise this gap, we develop a particularly expressive specification language, a calculus for stepwise refinement from such specifications down to distributed systems, and an automated tool for checking and supporting refinement steps in the calculus.Read moreRead less
Practical Automated Deduction. This project will develop, implement and validate improved methods for automated deduction in decidable fragments of first order logic, also incorporating reasoning in special theories such as arithmetic. It will significantly extend previous work on the model evolution calculus and dynamic semantic resolution, and introduce new techniques that combine these reasoning methods. This work has direct application to reasoning about business rules and about industrial o ....Practical Automated Deduction. This project will develop, implement and validate improved methods for automated deduction in decidable fragments of first order logic, also incorporating reasoning in special theories such as arithmetic. It will significantly extend previous work on the model evolution calculus and dynamic semantic resolution, and introduce new techniques that combine these reasoning methods. This work has direct application to reasoning about business rules and about industrial optimisation problems, and it will motivate and test our systems by means of case studies from both of these areas.Read moreRead less
Visual interaction methods for clustered graphs. This project aims to improve human understanding of huge network data sets, such as those arising in social networks, biological networks, and very large software structures. The project will enable analysts to explore and interact with such data sets, leading to better understanding.
Making software more reliable using a new model for entropies of computers' internal state. A new mathematical analysis of the way computer systems exchange data between their components has led to novel design approaches for the programs implementing those systems. This reduces their cost and increases their reliability, with improvements ranging from small-scale smart devices to widely distributed internet protocols.
Algorithms for geometric Turán-type problems and network visualization. Recent technological advances have large data sets, in a data deluge. Some of the most critical data sets are networks; examples abound in Systems Biology, Social Network Analysis, and Software Engineering. This project aims for algorithms to construct readable pictures of these networks, and thus make the data easier for humans to understand.
A formal foundation for security architecture. Security of computer systems is essential for the maintenance of privacy, confidentiality and integrity of personal, commercial and government data, and the trustworthiness of the computational devices that are embedded in critical societal infrastructure. However, current theoretical understanding of secure systems development is poor. The project will develop our understanding of an emerging approach to the design of secure systems and develop ver ....A formal foundation for security architecture. Security of computer systems is essential for the maintenance of privacy, confidentiality and integrity of personal, commercial and government data, and the trustworthiness of the computational devices that are embedded in critical societal infrastructure. However, current theoretical understanding of secure systems development is poor. The project will develop our understanding of an emerging approach to the design of secure systems and develop verification methods that may be applied to guarantee systems security. Its outcomes will contribute to processes for certifying systems at very high levels of security, a requirement in defence and government settings that will become increasingly significant in the commercial sector.Read moreRead less
Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop form ....Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop formally
based interoperability between the PVS and Maude systems, two widely
used computer tools for reasoning about complex systems.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
Approximate proximity for applications in data mining and visualization. Data Mining, pattern recognition and visualization of relational information are all important data analysis techniques in which it is essential to determine which data points are in the vicinity of others. The huge size of the data sets involved and the need for real-time interaction preclude the use of conventional methods for the precise computation of the proximity information required. This project will develop efficie ....Approximate proximity for applications in data mining and visualization. Data Mining, pattern recognition and visualization of relational information are all important data analysis techniques in which it is essential to determine which data points are in the vicinity of others. The huge size of the data sets involved and the need for real-time interaction preclude the use of conventional methods for the precise computation of the proximity information required. This project will develop efficient algorithms and data structures for gathering high-quality approximations of the full proximity information, and will use these innovations as the basis for new, practical tools for visualization, and clustering in data mining.Read moreRead less