AbsInt Astrée – Static Analysis Tool
Astrée is a static analyzer for C and C++ that enables engineering teams to prove the absence of runtime errors and invalid concurrent behavior in embedded software. Unlike traditional testing approaches, Astrée analyzes all possible execution paths across all possible inputs and environments. When no errors are reported, their absence has been formally proven. This makes Astrée particularly suited for safety-critical and mission-critical systems, where guarantees are required instead of assumptions.
Our brands
Our brands
Related articles
Embedded World 2026 Recap
Embedded World 2026 once again highlighted the rapid evolution of the embedded industry. From increasing focus on the Cyber Resilience Act (CRA) to the growing adoption of Zephyr OS, the...
Read more
The Top 5 Vulnerabilities in Embedded Software and How to Prevent Them
Read more
Why continuous monitoring for vulnerabilities is essential in embedded systems
Read more
PRESS RELEASE – McObject Launches eXtremeDB/rt 2.0: Breakthrough Persistent Hard Real-Time Database System Now Available to Logic Technology Clients
Read more
PRESS RELEASE – Logic Technology becomes exclusive Benelux distributor for IAR
Read more
What Astree analyzes
Astrée focuses on verifying runtime behavior at a deep semantic level. It detects and proves properties such as:
- Division by zero
- Out-of-bounds array access
- Invalid pointer usage (null, uninitialized, dangling)
- Integer and floating-point overflows
- Use of uninitialized variables
- Data races and concurrency issues
- Invalid system or OS calls
- Dead code and unreachable paths
- Violations of user-defined assertions
In addition, Astrée performs advanced analyses such as:
- Data-flow and control-flow analysis
- Signal-flow and taint analysis
- Component interaction and interference analysis
- Detection of specific vulnerabilities such as Spectre
General Features
Sound static analysis
If no errors are reported, their absence is formally proven.
High precision with minimal false alarms
Designed for large, real-world embedded systems.
Scalable performance
Efficient analysis of complex codebases.
Support for C, C++ and mixed codebases
Including modern C++ standards.
Compliance and certification support
Qualification support for standards such as ISO 26262, DO-178C and IEC 61508.
Integrated rule checking
Supports MISRA, AUTOSAR, CWE and custom coding rules.
Advanced reporting and collaboration
Detailed reports for certification and team workflows.
Toolchain integration
Command-line, CI/CD integration and plugins for common development environments.
Why Astree
For complex embedded systems, testing alone cannot provide full coverage or guarantees. Astrée enables a different approach:
From testing
to formal verification
From detecting errors
to proving their absence
From partial coverage
to exhaustive analysis
This results in:
Higher confidence
in software correctness
Reduced risk
of critical runtime failures
Stronger foundation
for certification processes
When to use Astree
Astree is most valuable in environments where:
Software failures have high impact
Certification is required
Systems include complex control logic or concurrency
Full coverage through testing is not feasible
Typical domains include aerospace, automotive, energy and other high-assurance embedded systems.
Gilbert Gadet
UEFI | BIOS | General Information
Want to understand if Astrée fits your development process?
I will help you determine not only when formal static analysis adds value, but also how to integrate Astrée into your workflow. Get in touch for tailored advice on Astrée and its application within your organization.
