Discover any divisions by zero, out-of-bounds array accesses, erroneous pointer manipulations, arithmetic overflows, data races, inconsistent locking, and other types of errors. Verify your code against MISRA, CWE, ISO/IEC and SEI CERT C coding guidelines, or your very own assertions.
Meet the highest levels of software assurance by compiling your application with the only C compiler that’s been formally verified to be free of miscompilation issues. All safety properties verified on the source code, e.g. with Astrée, are guaranteed to hold for the generated executable as well.
Compute tight upper bounds for the worst-case execution time of tasks in your binary executable. No testing or measuring required — the bounds are guaranteed to hold for every possible execution scenario, any combination of inputs, all cache and pipeline states.
Determine the worst-case stack usage of the tasks in your application. Find any stack overflows, or formally prove the absence thereof. Quickly identify critical sections and problematic execution paths to optimize your code’s performance.
Constantly monitor timing behavior during software development, even at the earliest stages. Identify bottlenecks when you haven’t even settled for a particular processor derivate yet, and measurements on physical hardware are plain impossible.
For information about custom-built, upcoming or discontinued products, contact firstname.lastname@example.org.