Our outpost runs a variety of projects related to static program analysis.
We are actively working on the Parfait and BegBunch projects and are also collaborating with academics at various universities.
Parfait is a static bug checking framework designed for scalability and precision. The Parfait tool checks C/C++ source code for common systems and security bugs. Parfait uses BegBunch and the OpenSolaris code base for nightly regression testing. The 8.6 million of lines of code of the OpenSolaris Operating System/Networking (ON) consolidation are analysed by Parfait in 20 mins on a 2.8GHz AMD Opteron machine.
BegBunch is a benchmarking suite for C bug checkers. BegBunch is composed of various benchmark suites to test correctness, accuracy and scalability of C bug checking tools.
The aim of this collaboration is to combine program analysis with model-based testing techniques to address issues of scalability and precision of bug checking tools, especially in the context of large systems code.
The aim of this Australian Research Council (ARC) Linkage project is to develop better methods for automatic static analysis of software to find latent errors and security loopholes, thereby improving the quality of code. The approach will make use of code annotations (such as assertions, invariants and extended type systems) to improve the precision of the program analysis process.
The aim of this collaboration is to develop static analysis techniques for analysing concurrent C/C++ software for scalability and precision. Bugs of interest include data races, deadlocks, livelocks, atomicity violations and serialisability violations, as well as concurrency-related security vulnerabilities.