AbsInt es un proveedor de herramientas de desarrollo de software con sede en Saarbrücken , Alemania . La empresa se fundó en 1998 como un spin-off tecnológico del Departamento de Lenguajes de Programación y Construcción de Compiladores del Prof. Reinhard Wilhelm en la Universidad de Saarland . AbsInt se especializa en herramientas de verificación de software basadas en interpretación abstracta . [1] Sus herramientas son utilizadas en todo el mundo por compañías Fortune 500, instituciones educativas, agencias gubernamentales y empresas emergentes.
aiT WCET Analyzer calcula de forma estática límites superiores seguros para el tiempo de ejecución en el peor de los casos [2] de tareas en sistemas en tiempo real . Analiza directamente los ejecutables binarios y tiene en cuenta la caché intrínseca y el comportamiento de canalización del microprocesador. [3] La Administración Nacional de Seguridad del Tráfico en las Carreteras de EE. UU. (NHTSA) y la NASA lo utilizaron en su Estudio sobre la Aceleración Involuntaria Súbita en los sistemas de control electrónico del acelerador de los vehículos Toyota. [4]
StackAnalyzer determina el uso máximo de pila de las tareas en aplicaciones integradas y puede probar la ausencia de desbordamiento de pila . Los resultados del análisis son válidos para todas las entradas y la ejecución de cada tarea. [5] StackAnalyzer se utiliza en las industrias aeroespacial, médica, de telecomunicaciones y de transporte.
Astrée es un analizador de programas estáticos que comprueba la ausencia de errores en tiempo de ejecución en aplicaciones integradas críticas para la seguridad escritas o generadas automáticamente en C . [6] Se utiliza en las industrias de defensa/aeroespacial, médica, control industrial, electrónica, telecomunicaciones/comunicación de datos y transporte. Astrée se origina en el grupo de Patrick Cousot en CNRS / ENS y es desarrollado y distribuido por AbsInt bajo licencia de CNRS/ENS.
RuleChecker es un analizador de programas estáticos que verifica automáticamente el código C/C++ para cumplir con las pautas de codificación, incluidas las pautas de codificación MISRA C /C++, SEI CERT C , CWE , ISO/IEC TS 17961:2013 y Adaptive Autosar C++.
TimeWeaver es una herramienta de análisis de WCET híbrida que combina el análisis de rutas estáticas y el análisis de valores estáticos con un seguimiento no intrusivo del nivel de instrucciones en tiempo real para limitar el tiempo de ejecución del peor de los casos ( WCET ). Este enfoque funciona para una amplia gama de procesadores modernos de alto rendimiento ( multinúcleo ).