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.

26. - 28. Februar 2019 // Nürnberg, Germany

Konferenzen und Rahmenprogramm

Zurück zur Tagesansicht
Session 6.6: Software Engineering V Software Quality II

Miscompilation – A Thing of the Past Vortragssprache Englisch

A compiler translates the source code written in a given programming language into executable object code of the target processor. Even in recent years scientific studies have found numerous bugs in all investigated open source and commercial compilers, including compiler crashes and miscompilation issues. Miscompilation means that the compiler silently generates incorrect machine code from a correct source program. In safety-critical systems this is a serious problem since it can cause erroneous or erratic behaviors including memory corruption and program crashes. CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. Source code and proofs are publicly available and are amenable to independent verification. This article gives an overview of the design and proof concept of CompCert. We will also report on experience gained at MTU Friedrichshafen in the context of a safety-critical industry application. The use of CompCert helped not only to improve the performance of the generated code, but also considerably reduced the (qualification) costs: using CompCert was a key factor for qualifying the engine control software according to IEC 60880, category A and IEC 61508-3:2010, SCL 3.

--- Datum: 28.02.2019 Uhrzeit: 14:00 Uhr - 14:30 Uhr Ort: Conference Counter NCC Ost

Sprecher

man

Dr. Daniel Kästner

AbsInt Angewandte Informatik GmbH

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.