AbsInt Astrée – Static Analysis Tool
Our brands
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
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.
Related articles
Lattix 2026.0 brings AI-assisted architecture analysis into the development workflow
Lattix 2026.0 brings AI-assisted architecture analysis into the development workflow with a new MCP Server, Ada support and improved automation.
Read more
Press-release: Logic Technology Now Distributes Razorcat TESSY Across the Benelux
Read more
Partner Insyde Software Launches TapRUUT™
Read more
Partner IAR Adds Long Term Support Option
Read more
Embedded World 2026 Recap
Read more
André De Ceuninck
Software Quality | Testing | Certification
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.
