[TYPES/announce] Postdoc position at University of Pennsylvania

Stephanie Weirich sweirich at cis.upenn.edu
Fri Sep 7 14:32:44 EDT 2012

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:


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 

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.

More information about the Types-announce mailing list