[TYPES/announce] Postdoc position at University of Pennsylvania
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:
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
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