Thesis Topic Details

Topic ID:
3212
Title:
Test vs Proof: The Showdown
Supervisor:
Gerwin Klein
Research Area:
Formal Methods, Operating Systems
Associated Staff
Assessor:
June Andronick
Topic Details
Status:
Active
Type:
R & D
Programs:
CE BIOM BINF SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
The ideal candidate has background in C, testing frameworks, and Isabelle/HOL.
Description:
The seL4 microkernel is formally verified to implement its specification. This verification by proof found 160 bugs in the C code of the kernel that were subsequently fixed. The question this thesis topic should answer is how many of these bugs would be found in a standard full coverage testing approach?

The task would be to take the original version of the kernel and achieve full coverage of all code paths in the kernel by testing and evaluate the results. The test cases could be partially or fully generated automatically from the formal specification.
Comments:
You will work in an international group of PhD students and researchers in the L4.verified and Trustworthy Embedded Systems projects in the Sydney/UNSW Laboratory of NICTA.
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.