The Coq mailing list

[Stephanie Weirich <sweirich AT cis.upenn.edu>]

We are currently seeking applicants for a post-doctoral position at 
the University of Pennsylvania with skills in programming language theory, 
proof assistants (Coq in particular), certified compilers such as 
CompCert, and logics for reasoning about low level programming languages.

This position is part of the DARPA funded project:

    SPARCS: SYNTHESIS OF PLATFORM-AWARE ATTACK-RESILIENT CONTROL SYSTEMS

The goals of the SPARCS project include: 

  * Design of control algorithms resilient to sensor and network attack

  * Synthesis of control software and proofs to guarantee the correctness of 
the system

  * Integration with certified operating system services

This position will focus on the latter two bullets and will involve 
using the Coq proof assistant for certified compilation of control software. 

The goal of SPARCS is to develop tools and techniques to ensure that a 
vehicle 
or systems of vehicles maintain a degree of control even when the system 
is under cyberattack. The particular focus of the Penn team is ground 
vehicles, 
including the Black-I Robotics Landshark and the GM Cadillac. This project is 
part of the HACMS program. More information at 
http://www.darpa.mil/Our_Work/I2O/Programs/High-Assurance_Cyber_Military_Systems_(HACMS).aspx

This project is a joint collaboration between the Penn programming language 
group (http://www.cis.upenn.edu/~plclub/) and the Penn PRECISE center for 
research in Embedded Computing and Integrated Systems 
(http://precise.seas.upenn.edu).  

For more information contact Stephanie Weirich at 
sweirich AT cis.upenn.edu.