Goanna Summer Projects

Have you ever wondered what research is about or whether you would be interested in a research career? To give you an opportunity to find out, the UNSW Faculty of Engineering has established the Taste of Research Summer Scholarships. For more information have a look at the web page.

Please, contact me if you are interested in or applied for a scholarship.

Overview:

• C/C++ Source Code Visualisation
• Compositional Concurrent Formal Modeling of Multi-threading
• Research on Explicit CTL Model Checking
• Automatic Computation of Software Quality Assurance Metrics
• Generic API and Visualization for Static Analysis Results
• Exploring SMT solvers for Software Analysis

Project Details

C/C++ Source Code Visualisation

Understanding software is a difficult task, this is in particular true for understanding source code. NICTA's Goanna project created an industrial strength bug checker that assists software developers in detecting defects and vulnerabilities automatically at compile time. However, for better understanding of the detected bugs a graphical display of source code is desirable. The goal of the summer project is to connect error traces in source code with graph visualisation software. This will enable a better understanding of why a bugs occurred and which parts of the code are impacted.

The project is in collaboration with a team of international researchers, engineers, and students and the novelty about this summer project is the merger of visualisation tools with static program analysis results.

Expected Outcomes: By the end of the summer project it is expected to have a prototype tool that takes current textual information such as control flow graphs, bug locations and error traces and maps those automatically to graph visualisation tools.

Compositional Concurrent Formal Modeling of Multi-threading

This summer project is related to the static C/C++ source code analyzer Goanna. The goal of the project is to build a compositional model of multi-threaded execution, which enables the modular analysis of multi-threaded software. The summer student will have to work on formal techniques such as assume-guarantee reasoning and compositional model checking. An understanding of concurrency and multi-threaded applications is a prerequisite.

The project is in collaboration with a team of international researchers, engineers, and students. The novelty is a new framework to efficiently analyze multi-threaded code and it will directly contribute to the industrial strength static analyzer Goanna.

Expected Outcomes: Co-development of a concurrency framework for multi-threading, proof-of-concept and sample implementation.

Research on Explicit CTL Model Checking

Model checking is an algorithmic way to analyze large annotated graphs with respect to certain properties. It has been used successfully in hardware verification and is now moving to software analysis. For hardware, symbolic model checking has proven to me most useful, however, this is not necessarily so for software. This summer project is about research in explicit state model checking for software, working on know implementations and comparing the result with existing symbolic solutions.

The project is in collaboration with a team of international researchers, engineers, and students.The novelty is to show that explicit state model checking can indeed be superior solution for software analysis. It will directly contribute to the industrial strength software analyzer Goanna.

Expected Outcomes: Investigation in explicit state model checking, implementation of algorithms, comparison to existing results.

Automatic Computation of Software Quality Assurance Metrics

This summer project is about researching software quality metrics and extending the C/C++ source code analyzer Goanna to compute those metrics automatically. The task is to investigate useful metrics to measure quality of code, both on developer level as well as on the quality assurance manager level, to build on the framework already implemented in the tool Goanna, and to design a solution for presenting the metrics information in an appealing way to the user. This will require some creativity.

The project is in collaboration with a team of international researchers, engineers, and students. The novelty will be in displaying software quality metrics based on source code analysis automatically to the developer in an appealing way. It will contribute to the industrial strength software analyzer Goanna.

Expected Outcomes:Investigation in software metrics, encoding selected metrics as rules in Goanna and displaying the metrics results.

Generic API and Visualization for Static Analysis Results.

This summer project is related to the static C/C++ source code analyzer Goanna. The goal of the project is to build develop a generic API for Goanna, which contributes to an easy integration in various Integrated Development Environments (IDE). Moreover, it should be investigated how software bugs and other related information can be best visualized in an IDE. The Visual Studio IDE will serve as a case study. Experience on plug-in development for Visual Studio is helpful.

The project is in collaboration with a team of international researchers, engineers and students. The summer project will develop a new solution to integrate analysis tools into IDEs and demonstrate how novel visualization techniques can effectively display software bugs.

Expected Outcomes: Investigation in API design, connection with visualization tools and implementation of interfaces.

Exploring SMT solvers for Software Analysis

Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combination of background theories such as reals, integers and various data structures. There are a number tools that solve these problems automatically. The goal of the summer project is to explore to which extend these SMT solvers can be used to analyze software such as C/C++ automatically. This project is targeted at students who have a good understanding of C/C++ code with a vivid interest in logics and/or mathematics.

The summer student will be embedded in the Goanna project team that created an industrial strength bug checker assisting software developers in detecting defects and vulnerabilities automatically at compile time. The team consists of international researchers, engineers, and students. So far there is little work on integrating SMT solvers in existing real-life software analysis tools. The project will significantly improve the current understanding in the field.

Expected Outcomes: By the end of the project a better understanding of SMT solvers, ideas for applying them to software source code, and estimations of their scalability are expected. These outcomes will contribute to the state-of-art research in this area.

Thesis Topics for Undergraduates

There are currently a number of topics available in the CSE thesis database. Search for my initials (RH) to find out more or contact me directly. Typically there are thesis opportunities in the area of the summer projects.

Also, most of the projects described above are thesis topics, but will go into more depth than a summer projects.

Other Thesis Topics

If you are interested in a Master or PhD thesis, please contact me directly.