3 ms·
Both. “They” (and by they I do not necessarily imply a large number of engineers at Airbus, but some people who are engineers at Airbus) use CompCert and “they”
by pascal_cuoq 11y ago
Both. “They” (and by they I do not necessarily imply a large number of engineers at Airbus, but some people who are engineers at Airbus) use CompCert and “they” also use Coq in order to finish up the correctness arguments for part of the properties that part of the software is supposed to have:
https://www.lri.fr/~marche/M2-TIP-Airbus.pdf https://www.lri.fr/~marche/M2-TIP-Airbus.pdf