Polyspace Alternative for EU Teams: Frama-C, Astrée, and CPAchecker on EU Infrastructure

Polyspace is a static analysis product from MathWorks — the Massachusetts company behind MATLAB and Simulink. It is widely used in European automotive and aerospace for ISO 26262 ASIL D and DO-178C Level A verification: proving absence of runtime errors, data races, and undefined behavior in safety-critical C and C++ code. Bosch, Continental, BMW, ZF, Airbus, and hundreds of Tier 1 DACH automotive suppliers use it as part of their certification evidence chain.

MathWorks is incorporated in the United States. Under the CLOUD Act, US authorities can compel MathWorks to produce data held anywhere in its infrastructure, regardless of where that data physically resides. For European teams running certification evidence, proof artifacts, and design data through Polyspace Cloud or on infrastructure connected to MathWorks services, this creates a jurisdiction exposure that is structurally identical to the one that caused the European Commission to stop using AWS in 2023.

This post covers the EU-native alternatives for each Polyspace use case, and what the migration path looks like for teams that need to keep certification evidence under EU jurisdiction.

What Polyspace Does

Polyspace has two main products:

Polyspace Bug Finder — static analysis for defect detection in C/C++. Identifies memory errors, data races, undefined behavior, MISRA C violations, and other defect categories. Aimed at the test and integration phase. Produces a list of bugs, not a proof.

Polyspace Code Prover — abstract interpretation based analysis that aims to prove absence of a defined set of runtime errors (called "red checks" and "orange checks") across all possible inputs and execution paths. For ISO 26262 ASIL D and DO-178C Level A, Code Prover is the tool used to produce the certification evidence that no runtime error can occur. This is the formal verification product.

The critical distinction: Bug Finder finds bugs. Code Prover produces proofs. The CLOUD Act concern is primarily about Code Prover outputs — the certification evidence files that form part of a safety case submitted to certification authorities.

The EU Alternatives

The EU formal methods ecosystem has deep coverage of every Polyspace use case. All three tools below originated in European academic institutions, are maintained by European teams, and — critically — can be self-hosted on EU infrastructure entirely outside US jurisdiction.

Frama-C — CEA/INRIA, Paris, France

Frama-C is a static analysis framework for C developed by CEA LIST (French Atomic Energy Commission) and INRIA in Paris. It uses a plugin architecture. The two plugins most relevant to Polyspace Code Prover users are:

WP (Weakest Precondition) — deductive verification plugin. You annotate C code with ACSL (ANSI/ISO C Specification Language) contracts, and WP generates proof obligations discharged by SMT solvers (Alt-Ergo, Z3, CVC5). This is the closest functional equivalent to Polyspace Code Prover: you prove that your code satisfies its specification, not just that it avoids a specific set of error patterns.

Eva (Evolved Value Analysis) — abstract interpretation plugin, the direct functional successor to a technique developed by Patrick Cousot at INRIA. Eva performs value analysis across all execution paths and reports a classification of all memory accesses, divisions, pointer arithmetic, and casts — proving absence of runtime errors for the analyzed scope.

Frama-C is qualified for use in DO-178C tool qualification at multiple avionics companies (Airbus, Thales, Dassault Aviation). EDF uses it for nuclear safety software verification to IEC 61508 SIL 4. It is open source (LGPL), maintained by CEA and INRIA teams in Paris, and trivially self-hostable on any Linux server.

For Polyspace Code Prover migration: Eva maps directly to the runtime error classification workflow. WP adds the capability to verify functional correctness beyond runtime error absence — a capability Polyspace Code Prover does not have.

Astrée — AbsInt, Saarbrücken, Germany

Astrée is the commercial abstract interpretation analyser from AbsInt GmbH, headquartered in Saarbrücken, Germany. It was developed by Patrick Cousot and Radhia Cousot at INRIA Paris (PLDI 2003), then commercialised through AbsInt.

Astrée's original claim was proving that the Airbus A380 primary flight control software — 132,000 lines of C — has zero runtime errors, with zero false alarms. AbsInt has since qualified Astrée for DO-178C Level A tool qualification, making it the highest-certified abstract interpretation tool in the EU market.

For Polyspace Code Prover users specifically, Astrée is the most direct replacement:

• Same soundness guarantee: all runtime errors reported, no false negatives
• Same output model: classification of alarm states (definitely red, possibly orange, definitely green)
• Same certification target: DO-178C Level A, IEC 61508 SIL 4, ISO 26262 ASIL D
• AbsInt is a German company under EU jurisdiction — no CLOUD Act exposure

The difference from Polyspace: Astrée is tuned for embedded C (no dynamic memory allocation, simple control flow) and excels in the zero-false-alarm result that certification authorities want to see. For complex C++ code with dynamic dispatch, the tradeoffs differ.

CPAchecker — LMU Munich, Germany

CPAchecker is a software verification framework from LMU Munich, developed by Dirk Beyer and the SoSy-Lab team. It is the multi-year champion of SV-COMP (Software Verification Competition) and the most configurable verification framework in the EU ecosystem.

Where Frama-C and Astrée focus on C, CPAchecker takes a broader approach: predicate abstraction with CEGAR (counterexample-guided abstraction refinement), k-induction, symbolic execution, and abstract interpretation are all pluggable analysis algorithms. For automotive teams running AUTOSAR-compliant C with complex control flow, CPAchecker's configurable framework is often a better fit than a fixed-algorithm tool.

CPAchecker is open source (Apache 2.0), runs entirely self-hosted, and has been used for ISO 26262 ASIL D verification at Bosch and Continental. The LMU Munich team publishes correctness witnesses — machine-checkable certificates of verification results — which enable independent validation of proof results, a capability no commercial static analysis tool offers.

Comparison: Polyspace Code Prover vs EU Alternatives

The Hosting Question for Certification Evidence

The CLOUD Act concern is not about the tool itself — it is about where the tool outputs live.

A complete Polyspace Code Prover run produces:

• A results database containing all alarm classifications
• A qualification report (for DO-178C tool qualification documentation)
• MISRA C compliance reports
• Coverage metrics tied to the analyzed source revision

For safety cases submitted to certification authorities — TÜV SÜD, DNV, Bureau Veritas, EASA — these artifacts are part of the certification record. They must remain intact and unmodified from the point of generation to the point of audit. If those artifacts are stored in, processed through, or transmitted via infrastructure with US jurisdiction, an adversarial legal process under the CLOUD Act could produce or modify them without your knowledge.

The same logic that applies to EU AI Act Article 9 proof artifacts applies here: the provenance and integrity of your safety case evidence matters. Under EN 50128, ISO 26262, and DO-178C, you must be able to demonstrate that your verification artifacts were produced by the tools you claim, in the configuration you claim, without modification.

EU-native infrastructure provides this chain of custody. A self-hosted Frama-C or Astrée instance on EU servers (no CLOUD Act exposure) provides a clean compliance argument that Polyspace Cloud or a Polyspace installation that phones home to Massachusetts does not.

Migration Path: What to Expect

The toolchain transition from Polyspace to EU alternatives is not trivial, but it is well-understood. The main migration steps are:

1. Audit your current Polyspace use cases. Most teams use Polyspace Bug Finder for development-phase defect finding and Code Prover for certification evidence. These map to different EU tools — Eva/CPAchecker for Bug Finder use cases, Astrée or Frama-C WP for Code Prover use cases.

2. Annotation investment. Frama-C WP requires ACSL annotations. If your C code has no existing contracts, adding them is work — typically 1-3 hours per module for complex code. Astrée and CPAchecker require less annotation for the basic runtime error absence proof.

3. Qualification documentation. AbsInt provides DO-178C Level A qualification documentation for Astrée. Frama-C has been qualified at several avionics companies with support from CEA. CPAchecker's correctness witness approach is recognized by SV-COMP but requires independent work for DO-178C qualification.

4. Infrastructure. All three tools run on standard Linux servers. Frama-C and CPAchecker are open source with no licensing constraints. Astrée requires an AbsInt license agreement. None require US cloud connectivity.

For teams already running on EU infrastructure with a CI pipeline, the integration path is straightforward. Frama-C and CPAchecker are available as Docker images and can be invoked as command-line tools in any CI system.

The EU Formal Methods Stack for Automotive

What makes the EU alternative stack coherent rather than fragmented is that these tools are designed to work together:

Frama-C + Why3 + Alt-Ergo — the full French deductive verification stack. All three tools are from INRIA/CEA/LRI groups in Paris and Saclay. Frama-C WP generates Why3 proof obligations. Alt-Ergo discharges them. This is the stack used at EDF, Airbus, and Thales.

CPAchecker + CBMC — the German bounded model checking + configurable program analysis stack. Both tools are used by Bosch and Continental. CPAchecker covers the full-program analysis; CBMC handles unit-level bounded model checking. TU Munich + University of Oxford, but CBMC is EU-operated in practice (Daniel Kroening is at Oxford, not a US company).

Astrée as drop-in — for teams that need a commercial, qualified, zero-configuration tool with the same output model as Polyspace Code Prover, Astrée from AbsInt (Saarbrücken) is the closest equivalent. AbsInt is a German company, fully EU jurisdiction.

EU CRA 2027 and the Supply Chain Argument

The EU Cyber Resilience Act requires CE-marked products to demonstrate vulnerability management and software supply chain transparency. For automotive software (which increasingly intersects with connected vehicles), the CRA supply chain requirements add another reason to audit where verification tooling lives.

A safety case that relies on verification evidence produced by a US-incorporated tool vendor is a supply chain element with US jurisdiction exposure. CRA Article 13 and Annex I Part II requirements for supply chain management create a documented reason to prefer EU-incorporated tool vendors for safety-critical verification.

Tools covered in this series:

• Frama-C: CEA/INRIA Paris, C Formal Verification on EU Infrastructure — deductive verification and abstract interpretation for C
• Astrée: AbsInt Saarbrücken, Zero False Alarms for Airbus A380 on EU Infrastructure — commercial abstract interpretation, DO-178C Level A qualified
• CPAchecker: LMU Munich, Configurable Program Analysis on EU Infrastructure — open source, SV-COMP champion, correctness witnesses
• EU Cyber Resilience Act 2027 and Formal Verification — CRA Annex I requirements and EU verification tool stack
• EU AI Act Hosting Compliance: Article 9 and Infrastructure Jurisdiction — why where you run verification matters

Run your static analysis and formal verification workloads on EU-native infrastructure with sota.io — hosted in Germany, operated under EU law, no CLOUD Act exposure.