Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.


Proof-carrying auto-coded control software

Proof-carrying code has been in existence since Necula and Lee coined the term in 1996. This talk brings forward the details of the development of proof-carrying code from control system specifications. The motivation for this work is the safety-critical nature of many control applications such as aeronautics, robot-assisted surgery, and ground transportation. Several challenges must be addressed during this effort, including: The formal representation of control-theoretic proofs; the migration and representation of these proofs across different layers of software implementation; and the design of a back-end to verify the claimed software properties. The expected payoff from these efforts is to include more semantics in the output of computer-aided control system design environments and to influence the software certification processes currently in use for transportation and health applications.

Type of Seminar:
Lecture Series on Directions in Systems and Control
Prof. Eric Feron
Aerospace Software Engineering, Georgia Institute of Technology, Atlanta, USA
Jan 30, 2012   14:15

ETZ E 6, Gloriastr. 35
Contact Person:

John Lygeros
File Download:

Request a copy of this publication.
Biographical Sketch:
Eric Feron is Dutton/Ducoffe Professor of Aerospace Engineering at Georgia Tech. His interests span air transportation, aerial robotics, engine control and flight testing, for which he leverages his background in applied mathematics, control systems and computer science. Prior to Georgia Tech, Feron was on the MIT faculty for twelve years. Feron is or has been on the editorial board of several journals. He enjoys sailing, skiing and biking.