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.) Sincerely, Demi
OpenPGP_0xB288B55FFF9C22C1.asc
Description: application/pgp-keys
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
