Please note: This master’s thesis presentation will take place in DC 2564.
Owen
Zila,
Master’s
candidate
David
R.
Cheriton
School
of
Computer
Science
Supervisor: Professor Nancy Day
Formal modeling is a powerful tool in requirements engineering. By modeling a system before implementation, one can discover bugs before they appear in testing or production. Model finding for a model written in first-order logic is the problem of finding a mapping of variables to values that satisfies a model’s specifications. Unfortunately, this problem is undecidable in general. Finite model finding, the problem of finding a mapping of variables to finite sets of values, is decidable. Thus, finite model finding enables the automated verification of models at certain scopes (the number of elements in the domain of discourse of the problem). When transforming a model into a problem for finite model finding, one runs into several challenges. While finitizing a problem makes it solvable, as the scope of the problem increases, the problem can quickly become prohibitively expensive to solve. Therefore, it is important to choose an efficient encoding of the problem for satisfiability (SAT) or satisfiability modulo theories (SMT) solvers when finitizing a problem.
We propose improvements to encodings of many-sorted finite model finding problems for SMT solvers. We propose new encodings for transitive closure and finite integers. The key contributions of this thesis are that we:
- Propose and prove the validity of an encoding of the transitive closure operator for a special case of the use of transitive closure
- Generalize existing encodings of transitive closure to relations of arity greater than 2
- Compare the performance of existing encodings and our new encoding of transitive closure on models generated from Alloy models
- Formulate Milicevic and Jackson’s (Milicevic 2014) method for preventing overflows in integer problems using bitvectors as a transformation from/to a many-sorted first-order logic formula
- Propose an integer finitization method, called overflow-preventing finite integers (OPFI), that produces results closer to unbounded integers than Milicevic and Jackson's method, improving the correctness of the finitization with respect to the same problem over unbounded integers
- Demonstrate that OPFI solves problems faster than our encoding of Milicevic and Jackson’s method in an SMT solver, and does not solve problems significantly slower than unchecked (pure) bitvectors