Diese Website verwendet Cookies, um das Angebot nutzerfreundlicher und effektiver zu machen. Mit der Nutzung dieser Website stimmen Sie der Verwendung von Cookies zu. Weitere Informationen über die Verwendung von Cookies und die Möglichkeit der Verwendung von Cookies zu widersprechen, finden Sie hier.

25. - 27. Februar 2020 // Nürnberg, Germany

Druckansicht einstellen

Welche Informationen sollen in der Druckansicht angezeigt werden?

Druckansicht erstellen
Aussteller & Produkte embedded world 2019

CompCert

Infos anfordern Infos anfordern

Kontaktieren Sie uns

Bitte geben Sie Ihre persönlichen Informationen und Ihren Terminwunsch an. Gerne können Sie uns auch eine Nachricht hinterlassen.

Ihre persönlichen Informationen

Ihre Nachricht an uns

Ihr Terminwunsch während der Messe

* Pflichtfelder, die von Ihnen eingegeben werden müssen.

Hinweise zum Datenschutz finden Sie hier.

Senden
Ihre Nachricht wurde erfolgreich versendet.

Sie haben noch keine Anmeldedaten? Registrieren Sie sich jetzt und nutzen Sie alle Vorteile der Aussteller- und Produktdatenbank, des Rahmenprogramms sowie des TicketShops.

Es ist ein Fehler aufgetreten.

CompCert ist ein formal verifizierter optimierender C-Compiler. Sein Einsatzbereich liegt in der Compilierung sicherheitskritischer C-Software, die hohen Zuverlässigkeitsanforderungen genügen muss. CompCert akzeptiert ISO C99 Programme und produziert Maschinencode für PowerPC (32-bit/64-bit hybrid), ARM, IA32 (x86 32-bit), AMD64 (x86 64-bit) und RISC-V.
 
Was ist das besondere an CompCert?
CompCert wurde durch maschinenunterstützte mathematische Beweise als korrekt bewiesen. Der Beweis zeigt, dass der vom Compiler produzierte Maschinencode dasselbe Verhalten aufweist, wie es die Semantik des C-Quellprogramms vorgibt. CompCert ist der erste kommerziell erhältliche formal verifizierte Compiler und bietet einen bislang unerreichten Vertrauensgrad in die Korrektheit des Übersetzungsprozesses.
 
Der formale Beweis deckt alle Transformationen vom abstrakten Syntaxbaum bis zum erzeugten Assembly-Code ab. Zum Präprozessieren und zur Erzeugung von Objektdateien und ausführbaren Dateien, werden externe Präprozessoren, Assembler, Linker und C-Bibliotheken verwendet. Diese Phasen sind somit unverifiziert, aber technisch wenig anspruchsvoll und aus Implementierungssicht robust, so dass sie gut durch traditionelle Qualifizierungskits abgedeckt werden können.
 
Die hohe Zuverlässigkeit von CompCert konnten schon anhand einer Entwicklungsversion von CompCert im Jahre 2011 in einer Studie von Regehr, Yang et al. nachgewiesen werden: “The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.”
 
Vorteile von CompCert:
* Kosten zum Aufspüren und Umgehen oder Beheben von Compilerfehlern und Auslieferung von Patches an die Endkunden des eingebetteten Systems können vermieden werden.
* Der Testaufwand zum Nachweis, dass bereits auf höheren Ebenen überprüfte Eigenschaften auch auf Maschinencode-Ebene gelten, kann reduziert werden, da dies automatisch aus dem Korrektheitsbeweis von CompCert folgt.
* In Bereichen, in denen bislang aus Sicherheitsgründen Compileroptimierungen ganz oder teilweise abgeschaltet wurden, können erstmals Compileroptimierungen eingesetzt werden.
* Auf typischen eingebetteten Prozessoren läuft der von CompCert generierte Code doppelt so schnell wie von GCC ohne Optimierungen erzeugter Code, und er ist nur 20% langsamer als GCC bei Optimierungsstufe 3. (Details über den verwendeten Benchmark-Mix, der diesen Zahlen zugrunde liegt, sind auf Nachfrage erhältlich.)

top

Der gewählte Eintrag wurde auf Ihre Merkliste gesetzt!

Wenn Sie sich registrieren, sichern Sie Ihre Merkliste dauerhaft und können alle Einträge selbst unterwegs via Laptop oder Tablett abrufen.

Hier registrieren Sie sich, um Daten der Aussteller- und Produkt-Plattform sowie des Rahmenprogramms dauerhaft zu speichern. Die Registrierung gilt nicht für den Ticket- und AusstellerShop.

Jetzt registrieren

Ihre Vorteile auf einen Blick

  • Vorteil Sichern Sie Ihre Merkliste dauerhaft. Nutzen Sie den sofortigen Zugriff auf gespeicherte Inhalte: egal wann und wo - inkl. Notizfunktion.
  • Vorteil Erhalten Sie auf Wunsch via Newsletter regelmäßig aktuelle Informationen zu neuen Ausstellern und Produkten - abgestimmt auf Ihre Interessen.
  • Vorteil Rufen Sie Ihre Merkliste auch mobil ab: Einfach einloggen und jederzeit darauf zugreifen.