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.