[TYPES/announce] PhD position in verification of low-level software

[Roberto Guanciale]

KTH the School of Computer Science and Communication (KTH CSC) invites
applications for a PhD position in verification of low-level
software.

We are seeking a PhD student in computer science with specialization
in software security to join the PROSPER project on provably secure
execution platforms for embedded systems. The objective of the project
is to build and verify low-level virtualization solutions. 
To realize this we work with formal verification
tools (theorem provers, low level program analysis tools), we build
hardware models, we develop the virtualization platforms and integrate
them with existing operating systems (Linux), and we apply the provers
and tools to high performance code at assembly or C level. The
specific role of the PhD student we are looking forward here is to be
determined, but will likely involve theory and tool development for
multicore processors. 

The successful candidate is expected to have a strong
foundational background in computer science (program logics and
program verification, machine architecture, operating systems,
programming) and mathematics (areas such as discrete mathematics,
formal logic). 

Application deadline: July, 6, 2014
Start date: September 2014

Details of the application procedure can be found on our website at:
http://www.kth.se/en/om/work-at-kth/vacancies/ph-d-student-in-verification-of-low-level-software-1.481486

For individual questions, the interested candidate is welcome to
contact Mads Dam (mfd at kth.se) or Roberto Guanciale (robertog at kth.se).