Final exam - Satisfiability Modulo Relations: Theory and Applications

Date: 
November 9, 2018 - 1:00pm
Location: 
137 SH

PhD Candidate: Baoluo Meng

Abstract

Many computational problems require reasoning about relational structures. Examples include high-level system design, architectural configuration of network systems, reasoning about ontologies, and verification of programs with linked data structures. Relational logic is an appealing choice for reasoning about such problems. As my thesis work, we presented a theory of finite relations (T_R) in satisfiability modulo theories (SMT) and also developed a calculus for that theory. We proved the correctness of the calculus that is refutation sound and model sound, and also proved the termination of the calculus for a fragment of T_R constraints. We also implemented the calculus as a theory solver in the SMT solver — CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling applications. For instance, native support for relations enables a natural mapping from Alloy, a declarative modeling language based on first-order relational logic, to SMT constraints. It also enables a natural encoding of several description logics with concrete domains, allowing the use of an SMT solver to analyze, for instance, Web Ontology Language (OWL) models. We developed translations from Alloy and OWL to SMT respectively, proved the correctness of the translations and provided experimental evaluations of the relational solver on Alloy and OWL benchmarks which show promising results. To speed up SMT solving in general, we introduced approaches for symmetry detection and breaking in SMT and proved its correctness.

Advisors: Cesare Tinelli