Formally Verified Software in the Real World. - KLEIN, GERWIN; ANDRONICK, JUNE; FERNANDEZ, MATTHEW; KUZ, IHOR; MURRAY, TOBY; HEISER, GERNOT (Communications of the ACM, 2018)
The article discusses the use of formally verified software to protect an autonomous helicopter against cyber attacks. Topics include the testing of vehicles by the U.S. Defense Advanced Research Projects Agency (DARPA) through its High-Assurance Cyber Military Systems (HACMS) program, the role of a trusted computing base (TCB) in computer architecture for security, and the componentization of systems.