PLC - 1 Verifying Mission-Critical Software

CSE Project - Associate Professor Albert Nymeyer (anymeyer@cse.unsw.edu.au) and Thang Hoai Bui (buih@cse.unsw.edu.au)

The aim of this work is to develop a tool to study program code and see whether the code satisfies particular properties. A starting point is a tool that has been developed at UNSW called Golfer. This tool will do a simple program analysis and throw away everything that it considers unimportant. The remaining program is called an `abstract' program. All the program executions (states) of the original program can then be searched (that could be a really large number) using the abstract program as a guide (called a heuristic).

The difficult part of this work is figuring out what is important in a program, because if the heuristic is bad (i.e. something important has been thrown away in the abstract program) the search will take forever. An example of a program analysis is to see how many times each variable is used, and only keep those variables that are used most often. This sometimes works well: but it is easy to find an example where it doesn't work. Understanding what works, and why, is what this research is about. Thang Hoai Bui is a PhD student who will be working closely with you.

Verification is a very important part of software development, particularly for software that is `mission critical'. A break-through in this area would have a major impact in the industry. An expected outcome of the research is a program analysis tool and verifier

For further information, please contact the supervisor.

PLC - 2 High-Performance Multidimensional Intensional Programming

CSE Project - Associate Professor John Plaice (plaice@cse.unsw.edu.au)

The TransLucid language is a recent invention of the Supervisor. It is a declarative language in which variables define values varying in a multidimensional space. The language has been used as the target language for the implementation of imperative programs, functional programs and logic programs. The objective of this research project is to develop compilation techniques to produce highly efficient implementations of TransLucid. The TransLucid language is the first formalism in which one can declaratively manipulate infinite data structures, higher-order functions and imperative programs. An expected outcome of this research is a compiler producing high-quality code for a number of different programming language paradigms.

For further information, please contact the supervisor.

PLC - 3 Multiparadigm Multidimensional Intensional Programming

SE Project - Associate Professor John Plaice (plaice@cse.unsw.edu.au)

The TransLucid language is a recent invention of the Supervisor. It is a declarative language in which variables define values varying in a multidimensional space. The language has been used as the target language for the implementation of imperative programs, functional programs and logic programs. The objective of this research project is to extend the work in programming language semantics pertaining to TransLucid in order to complete the translations of different programming language paradigms. The TransLucid language is the first formalism in which one can declaratively manipulate infinite data structures, higher-order functions and imperative programs. An expected outcome of the research is an intensional semantics for the common programming language paradigms. For further information, please contact the supervisor.

[Top of Page]