23 Nov
2020
23 Nov
'20
10:02 a.m.
On 23 Nov 2020, at 05:36, Matthew Fernandez <matthew.fernandez@gmail.com<mailto:matthew.fernandez@gmail.com>> wrote: Inria and Airbus have had success doing this since at least ~2005. If you want to read about this, Sandrine Blazy and Xavier Leroy have discussed it in some prior publications. Today I believe this process is supported commercially by the company AbsInt. AbsInt AFAIK does high-assurance worst-case execution-time (WCET) analysis, not general software assurance. But yes, Airbus has been a pioneer in formal verification of critical avionics software, for at least 30 years. Gernot