Document Type


Date of Degree

Fall 2013

Degree Name

PhD (Doctor of Philosophy)

Degree In

Computer Science

First Advisor

Tinelli, Cesare

First Committee Member

Stump, Aaron

Second Committee Member

Zhang, Hantao

Third Committee Member

Pemmaraju, Sriram

Fourth Committee Member

Barrett, Clark


In recent years, Satisfiability Modulo Theories (SMT) solvers have emerged as powerful tools in many formal methods applications, including verification, automated theorem proving, planning and software synthesis. The expressive power of SMT allows problems from many disciplines to be handled in a single unified approach. While SMT solvers are highly effective at handling certain classes of problems due to highly tuned implementations of efficient ground decision procedures, their ability is often limited when reasoning about universally quantified first-order formulas. Since generally this class of problems is undecidable, most SMT solvers use heuristic techniques for answering unsatisfiable when quantified formulas are present. On the other hand, when the problem is satisfiable, solvers using these techniques will either run indefinitely, or give up after some predetermined amount of effort. In a majority of formal methods applications, it is critical that the SMT solver be able to determine when such a formula is satisfiable, especially when it can return some representation of a model for the formula. This dissertation introduces new techniques for finding models for SMT formulas containing quantified first-order formulas. We will focus our attention on finding finite models, that is, models whose domain elements can be represented as a finite set. We give a procedure that is both finite model complete and refutationally complete for a fragment of first-order logic that occurs commonly in practice.


Finite Model Finding, Satisfiability Modulo Theories


vii, 150 pages


Includes bibliographical references (pages 145-150).


Copyright 2013 Andrew J. Reynolds