An Industrial Use-Case of Frama-C
This short video* was initially presented by Dillon Pariente from Dassault Aviation at the First International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'10).
It briefly presents the Frama-C platform and some of its main plug-ins. Additional details on the industrial usage of Frama-C at Dassault Aviation are presented in the related paper Formal Verification of Industrial C Code using Frama-C: a Case Study by Dillon Pariente and Emmanuel Ledinot which is included in the proceedings of the conference.
The Frama-C team is very grateful to Dillon Pariente from Dassault Aviation for making this video and making it freely available on our website.* A sound card is recommended.