Google Tech Talks June, 4 2008 ABSTRACT In this talk I will present the results of mathematically verifying third party flight control software. I will then present the results of mathematically verifying automatically generated code using The Mathworks code generation facilities and compare the cost against conventional development including V If time permits I will also present a small example of the form of the automatable formal verification of a specification in Simulink. The principles of the approach are generally applicable to other modelling languages that provide automatic code generation. Speaker: Colin O'Halloran Colin has worked in the area of Formal Methods for 25 years. He is a Visiting Professor at the University of York and a Visiting Fellow at Kellogg College Oxford University. He was a member of the European Space Agency's Board of Inquiry into the failure of Arianne 5's first flight. His current interests are in the commercial assurance of software.