logo slogan

AbsInt provides advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical software. Software testing accounts for a major part of development costs. This is especially true for real-time systems, where correctness depends not just on logical correctness, but also on the timeliness of the results. Timing properties are hard to establish; measuring and time-stopping methods are error-prone and time-consuming.

 

Static program analyses provide means to reduce testing and validation costs. The underlying theory of abstract interpretation enables the systematic derivation of provably correct analyses. The analyses are performed at compile time and provide results that hold for any program execution and any possible input scenario.

Phaedsys

Astrée Run time Errors

 

Finding all Runtime Errors and Data Races in C Programs: Astrée is a parametric static analyzer designed to prove the absence of runtime errors and data races in software programs written in C. Astrée is parameterizable and can be specialized to the program under analysis –key-features to enable high analysis precision. > Link to

Phaedsys

Rule Checker

 

RuleChecker is a static program analyzer that automatically checks your C or C++ code for compliance with MISRA rules, CERT recommendations, and other coding guidelines > Link to

Stack Analyser

StackAnalyzer automatically determines the worst-case stack usage of the tasks in your application. It lets you find any stack overflows, or formally prove the absence thereof. > Link to

aiT Worse Case Execution

aiT WCET Analysers statically compute tight bounds for the worst-case execution time (WCET) of tasks in real-time systems. They directly analyze binary executables and take the intrinsic cache and pipeline behaviour into account.. > Link to

Phaedsys

Timing Profiler

TimingProfiler helps you identify application parts that cause unsatisfactory execution times. It delivers results as soon as there is compiled code, and thus can be used very early in the development process, when measurements on physical hardware are costly or plain impossible.

This makes TimingProfiler ideally suited for constantly monitoring timing behaviour during software development and in model-based development environments. > Link to

Time Weaver

TimeWeaver combines static path analysis with timing measurements to provide worst-case execution time estimates.> Link to

Certified Compiler

 

CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, x86, and RISC-V architectures.. > Link to