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. Our research and education covers a wide area including natural sciences and all branches of engineering, as well as architecture, industrial management, urban planning, history and philosophy.
We are looking for postdoc candidates to conduct research within the expedition project “High-Confidence Formal Verification of Real Cyber-Physical Systems: from Models to Machine Code”.
The overall research goal of this project is to develop a new theoretical foundation of formally verified cyber-physical domain-specific model compilation, from high-level real system models down to machine code, satisfying both functional and temporal constraints. As part of this project, the challenge is to design and develop a verified model-checker and a synthesis mechanism that both verify the correctness of model properties and the translation down to executable machine code. The project will be conducted using the proof assistant Coq. The postdoc candidates are mentored by Associate Professor David Broman https://people.kth.se/~dbro/, who is leading the project at KTH. The overall project is a collaboration with Associate Professor Magnus Myreen’s group at Chalmers.
This position is a two-year position funded by the Wallenberg Artificial Intelligence, Autonomous Systems and Software Program (WASP). For more information, see http://wasp-sweden.org/17-post-doc-positions-expedition/.
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 reasons, for instance sick leave and parental leave). The candidate should have a strong background from at least one of the following areas: interactive theorem proving, real-time systems, or model checking. Although the research work will be done using the Coq proof assistant, there is no formal requirement of explicit Coq knowledge, but some prior experience with another interactive theorem prover is highly desirable.
The successful applicant should have an outstanding research and publication record. Well-developed analytical and problem solving skills are requirements. We are looking for a strongly motivated person, who is able to work independently. Good command of English orally and in writing is required to present and publish research results.
Great emphasis will be placed on personal competence and suitability.
Trade union representatives
You will find contact information to trade union representatives at KTH:s webbpage.
Log into KTH's recruitment system in order to apply to this position. You are the main responsible to ensure that your application is complete according to the ad.
Your complete application must be received at KTH no later than the last day of application, midnight CET/CEST (Central European Time/Central European Summer Time).
The application should contain the following:
Gender equality, diversity and zero tolerance against discrimination and harassment are important aspects of KTH's work with quality as well as core values in our organization.
For information about processing of personal data in the recruitment process please read here.
We firmly decline all contact with staffing and recruitment agencies and job ad salespersons.
Disclaimer: In case of discrepancy between the Swedish original and the English translation of the job announcement, the Swedish version takes precedence.
|Title||Postdocs in Verification of Cyber-Physical Systems using Proof Assistants|
|Employer||KTH Royal Institute of Technology|
|Job location||Valhallavägen 79, 100 44 Stockholm|
|Published||May 2, 2019|
|Application deadline||June 2, 2019|
|Job types||Postdoc  |
|Fields||Informatics,   Information Science,   Algorithms,   Artificial Intelligence,   Artificial Neural Network,   Computer and Society,   Computer Architecture,   Computer Communications (Networks),   Computer Graphics,    and 21 more. Cyber Security,   Computing in Mathematics, Natural Science, Engineering and Medicine,   Computing in Social science, Arts and Humanities,   Data Mining,   Data Structures,   Databases,   Distributed Computing,   Human-computer Interaction,   Information Systems (Business Informatics),   Operating Systems,   Parallel Computing,   Programming Languages,   Quantum Computing,   Software Engineering,   Theory of Computation,   Computational Sciences,   Game Design,   Big Data,   Machine Learning,   Machine Vision,   Computer Vision  |