Astrée ist ein statisches Analysetool, das die Abwesenheit von Laufzeitfehlern in sicherheitskritischem C/C++-Code nachweist (z. B. Datenwettläufe, Division durch Null, Feldzugriffe außerhalb der gültigen Feldgrenzen, ungültige Zeigermanipulationen und arithmetische Überläufe). Zudem trägt Astrée zum Nachweis von Wechselwirkungsfreiheit bei, berechnet Codemetriken und prüft die Einhaltung von MISRA C/C++, SEI CERT C/C++ sowie weiterer Codierrichtlinien. Mehr Info unter https://www.absint.com/astree/index_de.htm.

CompCert ist ein formal verifizierter optimierender C-Compiler. Er ermöglicht eine bislang unerreichte Zuverlässigkeit des Kompilierungsprozesses, die die höchsten Anforderungen der striktesten Standards erfüllt. Mehr Info unter https://www.absint.com/compce ...