[TYPES/announce] PostDoc in Verification of Simulink Models

[Dilian Gurov]

KTH is hiring one PostDoc in Verification of Simulink Models:

 
https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:265239/where:4/

Application deadline: May 16, 2019.
Starting date: August 1, 2019 (or by agreement).

The postdoctoral 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.

The postdoc will be responsible for developing a model-checking
based automatic verification technique for the exhaustive and
systematic verification of C modules developed by means of
Simulink models. The main challenge here is to cope with the
size and complexity of the industrial Simulink models, that
is, to find a technique that can be employed for verification
of intricate Simulink models with large state spaces.

The position is a full-time research position for one year.

Qualifications:
Applicants must hold or be about to receive a doctoral degree
in Computer Science (or equivalent). The doctoral degree must
have been obtained within the last three years from the application
deadline (some exceptions for special grounds, for instance
sick leave and parental leave). The candidate should have a
strong background in Computer Science, and in particular in
Formal Methods based on mathematical logic and models of program
behavior. Industrial experience, especially with Simulink and
embedded safety-critical software, is an advantage.

About KTH:
KTH Royal Institute of Technology in Stockholm has grown to
become one of Europe’s leading technical and engineering
universities, as well as a key centre of intellectual talent
and innovation. We are Sweden’s largest technical research and
learning institution and home to students, researchers and
faculty from around the world.