Smten

Development of tools for computer aided verification has greatly benefited from Satisfiability Module Theories (SMT) technologies; instead of writing an ad-hoc reasoning engine, tool developers translate their problem into SMT queries which solvers can efficiently solve. In practice, translating a problem into effective SMT queries is a tedious, error-prone, and non-trivial task. Smten is a unified language for general-purpose functional programming and SMT query orchestration whose goal is to greatly simplify the development of practical SMT-based tools for computer aided verification.

Smten is an open-source implementation of the Smten language as a plugin to the Glasgow Haskell Compiler which supports the full syntax of the Haskell functional programming language. Our implementation currently supports SMT solvers Yices1, Yices2, Z3, STP, and the SAT solver MiniSat.