[Работа]  PhD on modular verification and proof of cyber-physical systems (Inria & Mitsubishi, France)
Сообщение было послано: qwera (5x18x238x142.static-business.iz.ertelecom.ru)
Дата: Воскресенье, Апрель 14 13:26:54 2019


(repost from the mailing list concurrency@listserver.tue.nl)

Applications are invited for a doctoral project on the elaboration of a
logical framework to verify requirements of hybrid system models.

The goal of this project is to build cyber-physical systems with a
correct-by-construction approach in order to verify requirements against
both digital and physical aspects of such designs. Our approach is based
on components augmented with formal contracts that are expressed using
differential dynamic logic and can be composed, abstracted or refined. We
focus on automating proofs of system-level properties and requirements
from individual, possibly mechanized, proofs of component properties
(with, e.g., theorem provers, static analyzers). The envisioned framework
should, in the end, be usable by regular engineers (i.e. not proof theory
spe######ts) and tooled.

The ideal candidate will have a strong background in logic, concurrency,
proof, verification, and experience and interest in control theory and
embedded system design. The successful applicant will be employed by the
Industrial partner of the project: Mitsubishi Electric R&D Centre Europe,
under a three years CIFRE grant, and embedded with Inria project-team TEA
at Inria, Rennes (Brittany, France).

Detailed offer and complete information at
https://jobs.inria.fr/public/classic/fr/offres/2019-01424


Сообщения в этом потоке
+ [Работа]  PhD on modular verification and proof of cyber-physical systems (Inria & Mitsubishi, France) (url) (188) - qwera (5x18x238x142.static-business.iz.ertelecom.ru) - 14/4/2019 13:26
Ответить

Имя:   Пароль:    Автологин
Тема:
        

Отключить распознавание Тегов конференции
Отключить распознавание смайл-кодов
Получать уведомления об ответах по почте

 

Конференция основана на движке WWWConf 2.0 PRE BETA5, поддерживается и модерируется группой энтузиастов.