Email Gateway (Aug 22 2022 at 18:51): Email Gateway (Aug 22 2022 at 18:51):From: Magnus Myreen <myreen@chalmers.se>
We are looking to employ postdocs, one at KTH and one at Chalmers, to
conduct research in a joint expedition project titled:
High-Confidence Formal Verification of Real Cyber-Physical Systems:
from Models to Machine Code
The overall goal of this project is to develop new theoretical
foundations for formally verified cyber-physical domain-specific model
compilation, from high-level real system models down to machine code,
satisfying both functional and temporal constraints.
The project is a collaboration between:
Associate Professor David Broman at KTH, Sweden
https://people.kth.se/~dbro/
Associate Professor Magnus Myreen at Chalmers, Sweden
http://www.cse.chalmers.se/~myreen/
At KTH, this project will use the Coq proof assistant to design and
develop a verified model-checker and a synthesis mechanism that
correctly extracts an executable timed intermediate form (ETIF) from
high-level models of cyber-physical systems.
At Chalmers, this project will involve using the HOL4 interactive
theorem prover to develop a compiler partly from scratch and partly
from parts of the existing CakeML compiler. The new compiler's input
language is to be compatible with the ETIF from above.
To apply and read more, see the separate job ads:
Application deadline: 28 February, 2019
Starting date: preferably in the first half of 2019
Both postdoc positions are for two years. The funding comes from the
Wallenberg Artificial Intelligence, Autonomous Systems and Software
Program (WASP). For more information, see
http://wasp-sweden.org/17-post-doc-positions-expedition/.
Please contact David (dbro@kth.se) and Magnus (myreen@chalmers.se)
for more information.
Last updated: Apr 19 2024 at 20:15 UTC