[TYPES/announce] PhD Position in Deductive Verification of Safety-Critical Embedded Software

[Dilian Gurov]

The Theoretical Computer Science Group at KTH Royal Institute of 
Technology invites applications for a PhD position in Computer Science 
focusing on Deductive Verification of Safety-Critical Embedded Software. 
The doctoral position is within a collaboration project between KTH and 
Scania, and addresses the need for functional safety of embedded vehicle 
software. The project relies on formal verification techniques, such as 
deductive software verification and model checking. The two main 
problems that the project aims to solve are the problem of connecting, 
in a formal way, requirements at different systems levels, and the 
problem of automating the verification process. The first problem will 
be addressed by the development of a formal framework and tool for 
hierarchical software architecture modelling that encompasses the given 
requirements. The second problem will be addressed by the development of 
automated techniques and tools that read architectural specifications 
and, from these, automatically generate models and logical 
specifications for back-end verification tools.

This is a five-year full-time employed position involving 20% teaching. 
We are looking for strong candidates with background in Computer 
Science, and in particular in Formal Methods based on Mathematical Logic 
and Programming Language Semantics. Industrial experience, especially 
with embedded safety-critical software, would be an advantage.

See 
https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:239002/type:job/where:4/apply:1 
for the full announcement with more information and instructions on how 
to apply. The application deadline is December 31, 2018. Informal 
enquiries are welcome and may be sent to dilian at kth.se .

Dilian Gurov, Associate Professor
School of Electrical Engineering and Computer Science
KTH Royal Institute of Technology
https://www.csc.kth.se/~dilian/