Phd topics -
PhD student in formal program verification
Promoter: Prof. dr. ir. Bart Jacobs |
More info: jobsite
More info: https://icts.kuleuven.be/apps/jobsite/vacatures/id/53293212/lang/en
DistriNet is the premier research group in Belgium on distributed software and software security and collaborates actively with many peer research centers in Europe. Both the research group and the University of Leuven provide a dynamic and international working environment.
We are hiring a PhD student for research in the formal verification of safety and security properties of concurrent low-level systems code. For example, a goal is to be able to formally verify crash-freedom of parts of the Linux kernel. The likely platform for this research will be the VeriFast verification tool (http://distrinet.cs.kuleuven.be/software/VeriFast/).The DistriNet program verification team was recently awarded the prize for Best Team at the Formal Methods 2012 verification competition (http://distrinet.cs.kuleuven.be/news/2012/DistriNetTeamWinsVerifyThisCompetition.jsp).
This PhD project will aim toward industrial applicability but will have a strong theoretical underpinning; correspondingly, the student's skills and interests should include both concurrent low-level programming (in C) and theoretical developments in programming language metatheory (for precisely defining the proposed verification approaches and proving their soundness).
Standard Belgian PhD scholarship.
For more information please contact Prof. dr. Bart Jacobs, tel.: +3216372014, mail: email@example.com.
You can apply for this job no later than May 31, 2015 via the Click here to apply to this project