On our website, we would like to use the services of third-party providers who help us improve our promotional offerings (marketing), evaluate the use of our website (performance) and adapt the website to your preferences (functionality). We need your consent for the use of these services; you can always revoke this consent. You can find information about the services and the chance to reject them under “User-defined.” You can find additional information in our Data Protection Policy.

2 - 4 March 2021 // Nuremberg, Germany

Posting print layout

What information should be shown in the print layout?

Create print layout
Exhibitors & Products embedded world 2020


Request information Request information

Contact us

Please enter your personal information and desired appointment. You can also leave us a message.

Your personal information

Your message for us

Desired appointment during the exhibition

* Compulsory fields you must fill in.

Information on data protection can be found here.

Your message has been sent.

You do not have a registration yet? Register now and use all advantages of the Exhibitors and Products Database, the supporting programme and the TicketShop.

An error has occurred.

CompCert is a formally verified optimizing C compiler. Its intended use is the compilation of safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts ISO C99 programs and produces machine code for PowerPC (32-bit/64-bit hybrid), ARM, IA32 (x86 32-bit), AMD64 (x86 64-bit), and RISC-V.

What sets CompCert apart?

Unlike any other production compiler, CompCert is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. In other words, the code it produces is proved to behave exactly as specified by the semantics of the source C program.

This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.

The formal proof covers all transformations from the abstract syntax tree to the generated assembly code. To preprocess and produce object and executable files, an external C preprocessor, assemblers, linkers, and C libraries have to be used.  However, these unverified stages are well-understood and robust from an implementation perspective, hence they can be covered well by traditional qualification kits. The reliability of CompCert has been demonstrated on a development version of CompCert by a 2011 study by Regehr, Yang et al.:

“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.”

Your benefits

• Using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source-code level. The correctness proof of CompCert guarantees that all safety properties verified on the source code automatically hold for the generated code as well.

• On typical embedded processors, the code generated by CompCert typically runs twice as fast as the code generated by GCC without optimizations, and only 20% slower than GCC at optimization level 3. (Details about the benchmark mix used to obtain these numbers are available on request.)

• Costs for finding and avoiding or fixing compiler bugs and shipping patches to the customers of the embedded system can be avoided.


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.