TimingProfiler and CompCert: two new products by AbsInt

Saarbrücken, September 12th, 2015. AbsInt, a worldwide leading manufacturer of program analysis tools for safety-critical software, today has launched two new product lines.


TimingProfiler computes execution time estimates of programs without the need to repeatedly provide test inputs, execute, and measure. It is ideally suited for constantly monitoring timing behavior during software development and in model-based development environments.

TimingProfiler gives detailed information about the execution time and time-critical paths. Hotspots and bottlenecks can be identified at early development stages so that late-stage integration problems can be avoided.

TimingProfiler is initially available for PowerPC and TriCore. Support for further targets will be announced soon.

For further information, visit absint.com/timingprofiler.


CompCert is a formally verified optimizing C compiler. The verification has been done using machine-assisted math­ematical proofs, and shows CompCert to be exempt from miscompilation issues. In other words, the code it pro­duces is proved to behave exactly as specified by the semantics of the C source program.

The level of confidence in the correctness of the compilation process is unprecedented and helps meet the highest standards of software assurance.

Supported targets are PowerPC (32-bit), ARM, and IA32 (x86 32-bit).

CompCert was initially developed at INRIA, the French National Institute for computer science and applied mathematics, with contributions from numerous renowned researchers from all over the world. When in 2014 the compiler reached market-ready maturity, INRIA and AbsInt entered a license agreement to provide commercial licenses to end users. AbsInt will also provide industrial-strength support and maintenance, and continue to contribute to the advance­ment of the tool.

For further information, visit absint.com/compcert.

About AbsInt

AbsInt provides advanced development tools for embedded sys­tems, and tools for validation, verification and certification of safety-critical software. Its flagship products are aiT for worst-case execution time analysis, StackAnalyzer for static stack-usage analysis, and Astrée for proving the absence of run-time errors and invalid con­current behavior in safety-critical embedded app­lications.

For further information, visit www.absint.com.

Press contacts

Bärbel Faust, AbsInt
Phone: (+49 681) 383 60 14