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. |
||