Thesis Topic Details

Topic ID:
3214
Title:
Verifying the core of standard C library in Isabelle/HOL
Supervisor:
June Andronick
Research Area:
Formal Methods, Operating Systems
Associated Staff
Assessor:
Gerwin Klein
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE BIOM BINF SE
Group Suitable:
Yes
Industrial:
No
Pre-requisites:
An good understanding of C and some background in formal logic is essential. Experience with Isabelle/HOL is a plus.
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 Trustworthy Embedded Systems project at NICTA, building on the formally verified seL4 microkernel.
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.