|
|
Topic ID: |
738 |
Title: |
Verifying the core of standard C library in Isabelle/HOL |
Supervisor: |
Gerwin Klein |
Research Area: |
Formal Methods, Operating Systems |
|
Assessor: |
Ansgar Fehnker |
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 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. |
|
|
|---|
