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.
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.
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models