Taste of Research Summer Scholarships

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 Taste of Research Summer Scholarships. For more information have a look at the web page. The summer projects listed below are related to the L4.verified project.

Google for Theorems

Academic Supervisor: Gerwin Klein <gerwin.klein at nicta.com.au> (Formal Methods)
Co-Supervisor: Rafal Kolanski <rafalk at cse.unsw.edu.au> (Formal Methods)

Would it not be nice if your computer could search for truth instead of web pages of random trustworthiness? You can make it happen! The Isabelle theorem prover has a large library of mathematically proven facts and theorems, and the L4.verified project at NICTA has added over 6,000 of its own. There is much truth out there, the problem is finding it.

The Isabelle theorem prover already has a powerful built-in search function, but you need to understand and run the prover to use it. It is the task of this project to provide an easy-to-use web front-end to the prover's search mechanism in the spirit of Hoogle (a search engine for the standard library of the Haskell programming language). The result will make the knowledge of proven facts accessible to people unfamiliar with Isabelle and it will provide a huge productivity tool for the Isabelle theorem proving community specifically.

If the result of this project is evaluated to be suitable, it is possible that the front end will be used as a global search engine for the Isabelle distribution and the Archive of Formal Proofs. The project also can be extended in scope to lead into an honours level thesis.

This project is part of the verification of the L4 microkernel at NICTA. You will work with power users and developers of the Isabelle theorem prover in an international team of PhD students and researches in the NICTA Embedded, Realtime and Operating Systems group as well as the NICTA Formal Methods group.

This project is aimed at making theorem proving technology and results more accessible and to increase productivity for those who use it.

A good background in web technologies is required for this project. Familiarity with functional programming languages such as Haskell and ML is a plus.

Links:

The Top 100 Theorems

Academic Supervisor: Gerwin Klein <gerwin.klein at nicta.com.au> (Formal Methods)
Co-Supervisor: Thomas Sewell <tsewell at cse.unsw.edu.au> (Formal Methods)

Of the top 100 most famous and interesting mathematical theorems in the world, 80 have now been verified in an automated proof assistant, but only 69 in one theorem prover. Will we be able to get the full 100? This summer project consists of picking a small number of the easier and smaller ones of these famous theorems and prove them in the interactive, industrial grade theorem prover Isabelle. You will work under guidance and with the support of international experts in the theorem proving field.

If successful, your work has an excellent chance of bein published in either the Archive of Formal Proof or the Isabelle theorem prover distribution directly.

Although this is a fun project, it has the more serious background of driving interactive theorem proving technology and to make this technology more accessible to not-yet-experts. You will learn state of the art theorem proving technology that is also applied to program verification.

A good background in mathematics is required for this project. Links:

User interface for a high-performance, retargetable architecture simulator

Academic Supervisor: Gerwin Klein <gerwin.klein at nicta.com.au> (Formal Methods)
Co-Supervisor: David Cock <davec at cse.unsw.edu.au> (Formal Methods)

The aim of this project is to develop a user interface for debugging system-level code in our locally-developed retargetable architectural simulator. You will evaluate the available options (Eclipse plugin, www.eclipse.org vs. Custom-built GUI), take into account usability requirements, and then deliver a frontend module to integrate with the existing (Python based) runtime framework.

You will be working with an international project team (l4.verified/seL4), which is undertaking cutting-edge research in high reliability embedded systems.

When successfully completed, it is intended that this frontend will be used in the low-level implementation of the next-generation secure microkernel seL4, as well as on other embedded systems work within NICTA, and be included in a publicly-released open-source version.

Links:

Formal Verification of Linux

Academic Supervisor: Gerwin Klein <gerwin.klein at nicta.com.au> (Formal Methods)
Co-Supervisor: David Cock <davec at cse.unsw.edu.au> (Formal Methods)

The fully formal verification of Linux is slightly beyond the scope of a 3 month summer scholarship, but there is no reason why selected parts of the Linux kernel should not be amenable to formal verification in that time frame.

The aim of this project is to apply C-level formal verification techniques to a small Linux function of your choice and to evaluate how well the method is applicable to a larger code base.

You will be using a state-of-the-art C verification tool developed by the L4.verified project. The project will involve developing formal specifications and proofs of correctness in the the interactive theorem prover Isabelle/HOL.

You will be working with an international project team (l4.verified/seL4), which is undertaking cutting-edge research in high reliability embedded systems.

This work addresses the often neglected problem of verifying software written in system languages such as C. A successful outcome will provide useful experience in applied formal methods and increase the reliability of the Linux kernel.

Links: