GRASP/PRECISE Seminar: Eric Feron, Georgia Institute of Technology, “Proof-Carrying Auto-Coded Control Software”

Abstract: 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.