Next: Edinburgh
Up: Cooperating sites
Previous: Chalmers


Dassault Aviation

Dassault Aviation has put formal methods into industrial practice, especially formal specification and verification of safety critical embedded software. Our group investigated theorem proving techniques based on typed lambda calculi, using the Coq proof tool. (This choice was driven by tool-qualification issues, since correctness of software verification tools is a key issue for certification by Airworthiness Authorities.) Dassault Aviation funded a PhD student (Antonia Baala) in the Lemme Project at INRIA Sophia to improve the handling of non structural recursive functions in the Coq System (defended in 2002).

We are now using the Coq system to prove assertions on safety critical embedded C programs using the Why proof-obligations generator from Paris Sud. We intend to use Why extensively in the fall of 2003 and in 2004.

The senior members of the Programming Logic Group are



Bengt Nordström 2005-09-22