Home   >   Demonstrators   >   AGES

AGES

Demonstrator|vrain

Description
Automatic GEneration of order-sorted first-order logical modelS
Member
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

AGES allows to obtain models of first-order logic theories with multiple types (sorts) that can be hierarchically related (as subtypes). The tool obtains the models in a fully automatic way relying on linear algebra techniques and modulo propositional satisfiability theories (SMT). It is possible, however, to specify several possibilities for the generation of such models by setting selectable parameters in the web interface of the tool and also as part of the source files where the first order theory under consideration is represented.

POSSIBILITIES

Many program analysis tasks fit the following scheme: the program is encoded as a first-order theory and the property to be explored as a first-order formula. Property verification consists of finding a model for both (sometimes together with some additional component). This is the problem that AGES solves.

TECHNOLOGICAL ENABLER

Artificial Intelligence and Computing
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