Inicio   >   Demostradores   >   AGES

AGES

Demostrador|vrain

Descripción
Automatic GEneration of order-sorted first-order logical modelS
Miembro
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

AGES permite obtener modelos de teorías de la lógica de primer orden con múltiples tipos (sorts) que pueden estar relacionados jerárquicamente (como subtipos). La herramienta obtiene los modelos de forma totalmente automática apoyándose en técnicas de álgebra lineal y satisfacción proposicional módulo teorías (SMT). Es posible, sin embargo, especificar diversas posibilidades de generación de dichos modelos mediante el ajuste de parámetros seleccionables en la propia interfaz web de la herramienta y también como parte de los ficheros fuente donde se representa la teoría de primer orden que se está considerando.

POSIBILIDADES

Muchas tareas de análisis de programas encajan en el esquema siguiente: el programa se codifica como una teoría de primer orden y la propiedad a explorar como una fórmula de primer orden. La verificación de la propiedad consiste en encontrar un modelo para ambas (en ocasiones junto con algún componente adicional). Este es el problema que resuelve AGES.

HABILITADOR TECNOLOGICO

Inteligencia Artificial y Computación
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models