Many problems in formal program analysis and verification can be reduced to determining whether a logical theory (a set of logic formulas) derived from the program has a model, that is, whether there exists a structure that provides definitions for all constants, predicates, and function symbols that satisfy the formulas. Moreover, the actual description of such a model aids in tasks such as bounding a program’s complexity, or proving its termination.

This paper presents a linear algebra approach to generating models for theories in order-sorted first-order logic. The core idea is to interpret sorts as sets of numerical vectors, functions as linear combinations of such vectors, and predicates as linear relations, where functions and predicates can be piecewise defined by case distinction. More concretely, first, a parameterized structure is constructed from the theory, essentially a linear system of (in)equalities; second, a linear constraint solver is applied to determine values for the parameters such that the instantiated structure is indeed a model of the theory.

The paper systematically describes the mathematics behind the approach, but also demonstrates via a running example its application. The presented work builds on prior research on the termination analysis of term rewriting systems, but it generalizes it to a fully automatic framework for multi-sorted logic. This framework has been implemented in the AGES tool, which has been successfully used in various scenarios. Future work will also consider nonlinear structures and solvers over the general theory of real closed fields.