14
  • Halle 4 / Standnummer 4-138
Analyse und Kompilierung auf Quellcodeebene: Astrée und CompCert
Wichtige Fakten
  • Astrée findet alle Laufzeitfehler – garantiert.
  • Keine Compiler-Fehler mit CompCert – garantiert.
  • Astrée: Marktführende statische Analyse für Safety und Security.
Kategorien
Test- & Verifikations-Software Methoden & Werkzeuge für sichere Embedded Systeme Statische- & Laufzeit-Analysetools Sonstige Tools, Software

Produkt Information

  • 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 ...
    Download

    Sehen Sie sich unser Produktvideo an

    Default video thumbnail

    Analyse und Kompilierung auf Quellcodeebene: Astrée und CompCert Video