AbsInt

AbsInt is a 1998 spin-off from the Department for Programming Languages and Compilers at the Saarland University, where its founders had developed a generic and generative framework for binary-level static program analyzers and optimizers. An important component of this framework is the Program Analyzer Generator PAG, which allows to automatically generate static analyzers from a mathematical specification of the abstract domains and transfer functions. The first version of PAG was released in 1995. With PAG/WWW, a free academic version of PAG is available which has been used worldwide in numerous teaching courses.

In 2001, the StackAnalyzer product line for static stack usage analysis was launched, followed by the aiT WCET Analyzer product line in 2002. In 2004, only half a year after its launch, aiT was awarded a European Information Society Technology Prize for "groundbreaking products that represent the best of European innovation in information society technologies". In 2004, aiT was used to analyze the flight-control software of the Airbus A380, the world's largest passenger aircraft. In 2006, the Analyzers successfully passed the first WCET Tool Challenge carried out by Mälardalen University. In 2010, aiT and StackAnalyzer were integrated into SCADE Suite from Esterel Technologies, making it the first embedded-software development environment worldwide to feature WCET and stack analysis at the model level.

The development of Astrée started from scratch in November 2001 by Prof. Patrick Cousot at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by INRIA (Paris-Rocquencourt). Astrée stands for Analyseur statique de logiciels temps-réel embarqués ("real-time embedded software static analyzer"). It has been used successfully on the flight control software of the AIRBUS A340 and A380, where it raised no false alarms, even for complex computations involving floating-point numbers. In April 2008, Astrée was able to prove the absence of any runtime error in a C version of the automatic docking software of the Jules Verne Automated Transfer Vehicle (ATV) used for transporting payloads to the International Space Station. Since 2009 Astrée is commercially available from AbsInt under license from ENS/CNRS.

AbsInt has participated in many research projects funded by the European Commission and the German Ministry of Education and Research, such as DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, and others.

The name AbsInt is derived from abstract interpretation, a semantics-based methodology for static program analysis.

aiT WCET Analyzer statically computes safe upper bounds for the worst-case execution time of tasks in real-time systems. It directly analyzes binary executables and takes the intrinsic cache and pipeline behavior of the microprocessor into account. The U.S. National Highway Traffic Safety Administration (NHTSA) and NASA used it in its Study on Sudden Unintended Acceleration in the electronic throttle control systems of Toyota vehicles.

StackAnalyzer determines the maximum stack usage of the tasks in embedded applications and can prove the absence of stack overflow. The analysis results are valid for all inputs and each task execution. StackAnalyzer is used in the Aerospace, Medical, Telecom and Transportation industries.

Astrée is a static program analyzer that proves the absence of run-time errors in safety-critical embedded applications written or automatically generated in C. It is used in the Defense/Aerospace, Medical, Industrial Control, Electronic, Telecom/Datacom and Transportation industries. Astrée originates from the group of Patrick Cousot at CNRS/ENS and is developed and distributed by AbsInt under license from the CNRS/ENS. In the 6th Static Analysis Tool Exposition (SATE VI) of NIST (2020), Astrée was confirmed to satisfy the SATE VI Ockham Sound Analysis Criteria.

RuleChecker is a static program analyzer that automatically checks C/C++ code for compliance with coding guidelines including MISRA C/C++, SEI CERT C, CWE, ISO/IEC TS 17961:2013, and Adaptive Autosar C++ Coding Guidelines.