On 23 Nov 2020, at 05:36, Matthew Fernandez <matthew.fernandez@gmail.commailto: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