View article

We present an implemented programming language called LOIS, which allows iterating through certain infinite sets, in finite time. We argue that this language offers a new application of SMT solvers to verification of infinite-state systems, by showing that many known algorithms can easily be implemented using LOIS, which in turn invokes SMT solvers for various theories. In many applications, ω-categorical theories with quantifier elimination are of particular interest. Our tests indicate that state-of-the art solvers perform poorly on such theories, as they are outperformed by orders of magnitude by a simple quantifier-elimination procedure.