Tags:abstraction, logical models, program analysis and sorted first-order logic
Abstract:
We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. The tool systematically exploits (and relies on) the use of convex domains to associate domains to the different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted piecewise convex matrix interpretations. Relations interpreting binary predicates can be specified to be well-founded as an additional requirement for the generation of the model. The system is available as a web application.