Partners, AbsInt GmbH

AbsInt provides advanced development tools for embedded sys­tems, and tools for validation, formal veri­fication and certification of safety-critical software.

Background and mission

The embedded market of today is characterized by constantly rising soft­ware complexity and increasingly shorter time-to-market. The share of safety-critical applications is rising.

AbsInt’s tools are designed to:

• Enhance software safety
• Speed up time-to-market
• Lower testing and validation costs
• Improve software efficiency to reduce system costs for embedded, real-time, safety-critical applications
• Our tools are based on a generic and generative framework which allows an extremely quick, sound and flexible response to customer needs. This has been more than proven in a series of successful projects and by outstand­ing customer satisfaction.

Software testing accounts for a major part of development costs. This is especially true for real-time systems, where correctness depends not just on logical correctness, but also on the timeliness of the results. Timing properties are hard to establish; measuring and time-stopping methods are error-prone and time-consuming.

Static program analyses provide means to reduce testing and validation costs. The underlying theory of abstract interpretation en­ables the system­atic derivation of provably correct analyses. The analyses are performed at compile time and provide results that hold for any program execution and any possible input scenario.

AbsInt products :

CompCert C-Compiler for safety critical systems
CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It ac­cepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, x86, and RISC-V architectures. More here >>

Astrée, proving the absense of run-time errors
Our program analyzer Astrée, developed under license from CNRS/ENS, proves the ab­sence of run­time errors in C programs. Its extremely pre­cise and highly customizable ana­ly­sis engine enables find­ing all poten­tial run­time errors while keeping false alarms to a min­i­mum. Large-scale industrial safety-critical avionics software was suc­cess­fully analyzed with Astrée in just a few hours with zero false alarms.  More here >>

Timing validation for Real-Time software
Our award-winning aiT WCET Analyzer is the first software tool for ver­ifying that safety-critical applications always react fast enough. Since 2002, aiT is used by Airbus France for validating the timing behavior of critical avionics software. More here >>

Proving the absense of stack overflow
Our StackAnalyzer automatically computes the worst-case stack usage of the tasks in embedded applications. This re­duces develop­ment effort and helps prevent runtime errors due to stack over­flow. More here >>

Certification and qualification
Current safety standards such as ISO 26262, DO-178B/C, IEC-61508, EN-50125 and others require identifying potential functional and non-functional hazards and demonstrating that the software does not violate the relevant safety goals. More here >>

Abstract Interpretation : Sound verification, formal proof of correct results

Abstract-interpretation based tools such as aiT, StackAnalyzer, and Astrée provide formal veri­fi­cation with 100% complete and reliable results. They are therefore perfectly suited to be used for certification.

The qualification process is greatly simplified by our Qualification Support Kits. Additionally, Qualification Software Life Cycle Data Reports provide de­tails about our development processes.

Quick facts about AbsInt

Founded in 1998, AbsInt is a privately-held company with currently a 40-strong staff from four nations, all located at our headquarters in Saarbruecken, Germany. Our customers come from 40+ countries all over the world, including the United States, Canada, Japan, Russia, Australia and almost all member states of the EU. We have distribution agreements with major software distributors in Asia, North America, Middle East, and throughout Europe.

The company name is an acronym for “abstract interpre­tation”, a sophisticated approach to static program analysis formalized by Patrick and Radhia Cousot at the Laboratoire d’Informatique, Grenoble in 1977. It is by implementing this approach that we were able to develop our unique, highly successful products.

Learn more :

Please contact Gerard Fianen at INDES-IDS BV to learn more about the products, pricing and licensing models.