Thesis Topic Details

Topic ID:
738
Title:
Verifying the core of standard C library in Isabelle/HOL
Supervisor:
Gerwin Klein
Research Area:
Formal Methods, Operating Systems
Associated Staff
Assessor:
June Andronick
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
An good understanding of C and some background in formal logic is essential. Experience with Isabelle/HOL or having heard COMP4161 is not required, bu
Description:
You will work with a state-of-the-art interactive theorem prover (Isabelle/HOL) to formally verify the functional behaviour of a small number of basic C functions like memcpy, memset, etc. The verification of these functions is at the basis of any undertaking that wants to provide guarantees about programs implemented in C.

This project is an integral and important part of the formal verification of the seL4 micro kernel at NICTA. You will work with the developers of L4 and Isabelle in an international team of PhD students and researchers in the NICTA Embedded, Real Time, and Operating Systems program and the NICTA Formal Methods program.
Comments:
You will work as part of a significant research project with a team of international PhD students and researchers at NICTA Kensington.
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.