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.Bio:
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, Dr. Feron was on the MIT faculty for twelve years. He is or has been on the editorial board of several journals. He enjoys sailing, skiing and biking.