Alt-Ergo

Alt-Ergo , un solucionador automático de fórmulas matemáticas , se utiliza principalmente en la verificación formal de programas . Funciona según el principio de satisfacibilidad módulo teorías (SMT). Su desarrollo fue llevado a cabo por investigadores de la Universidad Paris-Sud , el Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France y el CNRS . Desde 2013, la gestión y supervisión del proyecto corren a cargo de la empresa OCamlPro. ^[¹^] Se distribuye bajo la licencia de software libre y de código abierto CeCILL-C.

Tecnologías

Opciones de diseño

Alt-Ergo emplea un lenguaje de entrada especializado con polimorfismo prenexo , diseñado para reducir la cantidad de axiomas que requieren cuantificación y simplificar la complejidad de los problemas. Si bien Alt-Ergo ofrece soporte parcial para el lenguaje SMT-LIB 2, su eficiencia con archivos SMT es relativamente limitada.

Componentes principales

La arquitectura central de Alt-Ergo consta de tres elementos principales: un solucionador SAT basado en búsqueda en profundidad (DFS) , un motor de instanciación de cuantificadores que utiliza la coincidencia electrónica (e-matching ) y un conjunto de procedimientos de decisión para diversas teorías integradas. Estos componentes, en conjunto, permiten a Alt-Ergo resolver fórmulas automáticamente.

Teorías incorporadas

Alt-Ergo implementa procedimientos de (semi)decisión para las siguientes teorías:

Teoría vacía
Aritmética lineal de enteros
Aritmética racional lineal
Aritmética no lineal
Aritmética de punto flotante
Matrices polimórficas
Tipos de datos enumerados
Símbolos de CA
Tipos de datos de registro

Usos industriales

Varias plataformas de verificación están construidas sobre Alt-Ergo:

Why3 , una plataforma para la verificación deductiva de programas, utiliza Alt-Ergo como probador principal ^{[ 2 ].}
CAVEAT, un verificador C desarrollado por CEA y utilizado por Airbus; Alt-Ergo se incluyó en la calificación DO-178C de una de sus aeronaves.
Frama-C , un marco para analizar código C, utiliza Alt-Ergo en los complementos Jessie y WP (dedicados a la verificación deductiva de programas ).
SPARK utiliza Alt-Ergo (detrás de GNATprove) para automatizar la verificación de algunas aserciones en Spark 2014.
Atelier-B puede usar Alt-Ergo en lugar de su probador principal (aumentando el éxito del 84% al 98% en los benchmarks del proyecto ANR Bware ).
Rodin , un marco de trabajo basado en el método B desarrollado por Systerel, puede utilizar Alt-Ergo como backend.
Cubicle , un verificador de modelos de código abierto para comprobar las propiedades de seguridad de los sistemas de transición basados en matrices.
EasyCrypt , un conjunto de herramientas para razonar sobre propiedades relacionales de cálculos probabilísticos con código adversario.
BWARE ^{[ 3 ]}
Cafeína ^{[ 3 ]}
FUI Hi-Lite ^{[ 3 ]}
Decert ^{[ 3 ]}
ADT Alt-Ergo ^{[ 3 ]}
A3PAT ^{[ 3 ]}

Véase también

Referencias

↑ "Acerca de" . alt-ergo.ocamlpro.com . Consultado el 15 de junio de 2023 .
↑ "Why3" . why3.lri.fr. Consultado el 15 de junio de 2023 .
1 2 3 4 5 6 "El demostrador de teoremas Alt-Ergo: Página web académica" . alt-ergo.lri.fr . Consultado el 15 de junio de 2023 .

Enlaces externos

Sitio web oficial , OcamlPro
Alt-Ergo en LRI

[1] "Acerca de" . alt-ergo.ocamlpro.com . Consultado el 15 de junio de 2023 .

[2] "Why3" . why3.lri.fr. Consultado el 15 de junio de 2023 .

[:0-3] 1 2 3 4 5 6 "El demostrador de teoremas Alt-Ergo: Página web académica" . alt-ergo.lri.fr . Consultado el 15 de junio de 2023 .

[

[ 2 ].