AbsInt

Enhancing Embedded Software Verification in Israel with ITEC

Introduction

Founded in 1998 as a spin-off from Saarland University, Germany, AbsInt Angewandte Informatik GmbH is a leader in software-verification tools grounded in the theory of abstract interpretation.

Today, AbsInt's products serve industries worldwide—ranging from aerospace and automotive to medical and industrial automation—by enabling rigorous, sound static analysis of embedded and safety-critical software.

Why AbsInt Matters for Embedded Systems

In embedded development, correctness extends beyond functionality to include timeliness, memory safety, and reliability under all input conditions. Traditional testing cannot guarantee this exhaustive coverage. AbsInt tools fill this gap by delivering provably correct results—they guarantee coverage across all possible executions using abstract interpretation.

Core Products & Capabilities

Here’s an overview of AbsInt's flagship tools and how they elevate embedded development:

1. Astrée

A sound static analyzer for C/C++ applications, Astrée proves the absence of run-time errors in safety-critical code—such as buffer overflows, divisions by zero, or data races. It has been used successfully in aerospace on Airbus A340/A380 systems with zero false alarms.

2. aiT WCET Analyzer

Computes tight and safe upper bounds for Worst-Case Execution Time (WCET) directly from binary executables, taking cache and pipeline behavior into account. It’s crucial for real-time systems and has been adopted by NHTSA and NASA in investigations of Toyota throttle control systems

3. StackAnalyzer

Determines the maximum stack usage for tasks in embedded applications and can formally prove the absence of stack overflows—key for safety-critical systems. Used across aerospace, medical, telecom, and transportation industries.

4. RuleChecker

A static analyzer that automatically checks C/C++ code for compliance with industry coding standards, including MISRA C/C++, SEI CERT C, CWE, and AUTOSAR guidelines.

5. TimeWeaver

A hybrid analysis tool combining static path analysis and real-time instruction-level tracing to bound WCET, especially suited for modern multi-core processors.

6. CompCert

A formally verified optimizing C compiler that ensures the compiled code precisely matches the source semantics. CompCert supports architectures like ARM, PowerPC, x86, and RISC-V and earned the 2021 ACM Software System Award.

Why Choose AbsInt Tools?

ITEC’s Role as AbsInt’s Representative in Israel

At ITEC Ltd, we are proud to represent AbsInt in Israel, bringing these sophisticated static analysis tools to local developers of embedded, real-time, and safety-critical systems. Our support includes:

• Technical assistance and demos: Providing hands-on guidance tailored to your project needs.
• Training: Enabling teams to effectively integrate tools like aiT, Astrée, or CompCert into their workflows.
• Qualification support: Helping customers navigate the ISO/IEC certification process with AbsInt’s Qualification Support Kits.

Real-World Applications

• Automotive Safety: Ensuring embedded systems comply with ISO 26262 by verifying WCET, stack safety, and eliminating run-time errors.
• Aerospace Reliability: Validating avionics code with Astrée and aiT for flight control and real-time execution.
• Medical Embedded Control: Ensuring robust, error-free operation in software governing critical medical devices.
• Industrial Automation: Maintaining rigorous timing and stability in controllers, PLCs, and embedded automation systems.

Conclusion

AbsInt equips embedded systems engineers with unmatched tools for provably safe, reliable, and certifiable software development—tools that address timely performance, memory safety, and predictability in ways conventional testing cannot. With ITEC Ltd as your local partner, Israeli teams gain direct access to expertise, licensing, and support needed to drive embedded innovation with confidence.