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.
Eric Feron has been the Dutton-Ducoffe Professor of Aerospace Software Engineering at the Georgia Institute of Technology since 2005. Prior to that, he was on the faculty of MIT's department of Aeronautics and Astronautics from 1993 until 2005. He holds his BS, MS and PhD degrees from Ecole Polytechnique, France, Ecole Normale Suprieure, France and Stanford University, United States. Eric Feron's interests are to use fundamental concepts of control systems, optimization and computer science to address important problems in aerospace engineering, including: Aerobatic control of unmanned aerial vehicles, multi-agent operations, including air traffic control systems and aerospace software system certification. Eric Feron has published two books and several research papers; his former research students are distributed throughout academia, government and industry. He is an advisor to the Academy of Technologies, France. When he is not in his office, Eric Feron may be found sailing along the coast of Florida.