[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 [email protected] .
Dilian Gurov, Associate Professor
School of Electrical Engineering and Computer Science
KTH Royal Institute of Technology
https://www.csc.kth.se/~dilian/
