This website uses cookies to make the content more user-friendly and effective. By using this website, you agree to the use of cookies. You can find additonal information about the use of cookies and the possibility of objecting to the use of cookies here.

25 - 27 February 2020 // Nuremberg, Germany

Conferences and supporting programme

back to day overview
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.

--- Date: 28.02.2019 Time: 14:00 - 14:30 Location: Conference Counter NCC Ost



Dr. Daniel Kästner

AbsInt Angewandte Informatik GmbH


The selected entry has been placed in your favourites!

If you register you can save your favourites permanently and access all entries even when underway – via laptop or tablet.

You can register an account here to save your settings in the Exhibitors and Products Database and as well as in the Supporting Programme.The registration is not for the TicketShop and ExhibitorShop.

Register now

Your advantages at a glance:

  • Advantage Save your favourites permanently. Use the instant access – mobile too, anytime and anywhere – incl. memo function.
  • Advantage The optional newsletter gives you regular up-to-date information about new exhibitors and products – matched to your interests.
  • Advantage Call up your favourites mobile too! Simply log in and access them at anytime.