A 12 year Dormant Error found in just 1.474 seconds!

The Applied Formal Methods course featured an excellent guest talk by Dr. Yogananda Jeppu of Honeywell on February 9, 2017. For illustration purposes, Dr. Jeppu demonstrated using CBMC to analyze a flight control system with a bug in it that could be triggered by a normal sequence of actions by the pilot, and showed how a 12-year dormant error was found in just 1.4 seconds. Thanks to Yoga Jeppu for contributing yet another compelling example of how formal analysis could have easily and efficiently prevented an error that later disrupted a critical avionics system during flight.