Proof Theoretical Methods for Reasoning about Process Equivalence. The emergence of internet commerce has made the issue of secure computing more urgent than ever. A substantial part of the security issues with today's computer applications are due to design problems.
The principles of secure computation have not been fully understood and adequate tools for the construction of secure applications are still lacking. The understanding of the foundations of secure computation is essential in bu ....Proof Theoretical Methods for Reasoning about Process Equivalence. The emergence of internet commerce has made the issue of secure computing more urgent than ever. A substantial part of the security issues with today's computer applications are due to design problems.
The principles of secure computation have not been fully understood and adequate tools for the construction of secure applications are still lacking. The understanding of the foundations of secure computation is essential in building trusted computer applications. Process calculi and logic represent two promising disciplines in which the principles of analysis and design of secure systems can be studied systematically, out of which formal verification tools can be constructed.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.
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
Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers a ....Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers access to powerful logical techniques in those applications. In the process, fundamental problems in modelling multiple granularity of time will be identified, and application-independent solutions to those problems will be provided.Read moreRead less
Adapting the Bulk Synchronous Parallel processing model to Peer-to-Peer Networked Computing. Advances in distributed computing have shown that data parallel and parametric applications domains are amenable to wide area distribution. The project will advance the Bulk Synchronous Parallel processing model to describe innovative applications from the loosely synchronous domain, e.g. fluid dynamics, strategy algorithms and N-body problems are challenges that have significant scientific and industria ....Adapting the Bulk Synchronous Parallel processing model to Peer-to-Peer Networked Computing. Advances in distributed computing have shown that data parallel and parametric applications domains are amenable to wide area distribution. The project will advance the Bulk Synchronous Parallel processing model to describe innovative applications from the loosely synchronous domain, e.g. fluid dynamics, strategy algorithms and N-body problems are challenges that have significant scientific and industrial value. The project specializes the exciting peer-to-peer paradigm, a frontier of inter-networking technology. By using the latest techniques and taking advantage of the technology implosion caused by low cost parallel infrastructure, the project outcomes will give Australia a strong position in the future of parallel technology.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
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
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
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