ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper). Cassez, F. & Sloane, A. In SCALA'17, October 23–27, 2017, Vancouver, BC, Canada. Proceedings., 2017. Association for Computing Machinery. forthcoming
ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper) [pdf]Paper  abstract   bibtex   3 downloads  
A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether a logical formula is satisfiable. The performance of SMT solvers has dramatically increased in the last decade and for instance, many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, thereby isolating users from the details of particular solvers.

Downloads: 3