The Coq mailing list

[Magnus Myreen <myreen AT 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:
 - KTH: https://goo.gl/f9HheP
 - Chalmers: https://goo.gl/SB8V3X

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 AT kth.se)
 and Magnus 
(myreen AT chalmers.se)
for more information.