> On Nov 22, 2020, at 10:43, Demi M. Obenour <[email protected]> wrote: > > On 11/22/20 1:36 PM, Matthew Fernandez wrote: >> >>> On Nov 22, 2020, at 10:01, Demi M. Obenour <[email protected]> wrote: >>> >>> (Speaking of avionics: is it possible to scale formal verification >>> to systems of that scale? I would love to see formally-verified >>> avionics software.) >> >> 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. > > Is this full functional verification, or “merely” proving freedom > from runtime errors? (Quotes because proving freedom from runtime > errors is still a substantial victory.)
That I do not know. You would have to read their papers or ask the authors. _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
