AbsInt
Proving Software Safety for Aerospace Certification

Software verification in aerospace extends beyond testing individual scenarios, particularly when safety depends on understanding behaviour across possible inputs and execution conditions that conventional testing cannot fully cover. Runtime errors, data races, stack overflows, timing bottlenecks and memory-safety issues can remain outside the reach of finite test cases, making full data and path coverage crucial for safety-critical software.

AbsInt develops static analysis and formal verification tools, helping aerospace organisations examine software behaviour. The analysis provides mathematically sound results for all possible inputs and execution scenarios, supporting software verification and certification. Rigorous analysis can fit the engineering environment already in use.

“Our goal goes beyond finding bugs,” says Dr. Christian Ferdinand, CEO. “We aim to formally prove their absence, giving aerospace teams the confidence to build, verify and certify software.”

The technology is used by organisations including Airbus, ATR, OHB, ESA, Thales Alenia Space and NASA.

Turning Analysis into Certification Evidence

AbsInt takes its name from abstract interpretation, the formal method underlying its core analysis technology. The method uses safe yet minimal overapproximation to analyse complex software systematically while preserving mathematical soundness when determining whether software behaviour can be considered safe.

Its approach rests on a simple principle expressed through its motto, ‘always on the safe side.’ If precision is insufficient to establish safety, the analysis raises a potential issue rather than overlooking it.

For aerospace teams, however, establishing a verification result is only part of the process. The analysis also supports certification under standards including DO-178C, DO-333 and DO330. Qualification Support Kits provide a structured route for turning analysis into qualification evidence.

Each kit covers requirements, test cases, procedures, traceability, test suites, execution frameworks and tool lifecycle data. The resulting qualification evidence can be integrated directly into certification documentation, helping simplify the path from analysis to certification within established programs.

“Our experience has shown that customers need more than an analysis engine. They need trustworthy results, a clear path to certification and practical support,” says Dr. Daniel Kästner, CTO.

Built for Diverse Technical Environments

Three decades of involvement in aerospace and space projects have helped AbsInt turn advances in software verification into practical tools for real-world certification environments.

Aerospace programs use different processors, compilers and software architectures, requiring verification technology to adapt without forcing engineering teams to replace the tools and processes already in use. AbsInt’s generic and extensible analysis framework supports architectures including PowerPC, x86, LEON, RISC-V, ARM and TriCore, as well as more than 20 others. Bespoke adjustments are also available for specific customer requirements.

Compiler support includes GCC, GNAT, LLVM, Diab, Tasking, GHS and CompCert. AbsInt also integrates verification with existing development environments through Jenkins, TargetLink and Visual Studio Code. Batch operation, automated data exchange and XML-based workflows incorporate verification into established development and continuous-integration processes rather than requiring separate infrastructure.

Applying Formal Verification in Aviation

The practical value of AbsInt’s approach becomes clear when formal verification must support an actual aircraft certification program. A recent application involving the MFC_NG generation of ATR 42 and ATR 72 aircraft involved the use of an optimising C compiler for critical avionics software alongside the assurance and certification evidence demanded by DO-178C.

AbsInt supported deployment of the formally verified CompCert compiler, providing the commercial product, industrial support and qualification expertise required for the application. CompCert’s compilation process is mathematically proven correct, eliminating miscompilation risks and reducing development effort within the certification program.

The ATR 42 and ATR 72 program achieved successful compiler qualification supporting DO-178C DAL A through DAL D, allowing certification credit from the compiler’s formal verification. The program now uses a qualified compiler combining high assurance with practical performance benefits.

As aerospace software continues to evolve, the company continues to develop practical verification tools that help teams build, verify and certify the next generation of safety-critical software.