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
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.
@inproceedings{scala-17,
author = {Franck Cassez
and {Anthony M.} Sloane},
title = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},
booktitle = {SCALA'17, October 23--27, 2017, Vancouver, BC, Canada. Proceedings.},
pages = {},
year = {2017},
xxxurl = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},
xxxdoi = {10.1007/978-3-662-46681-0_39},
publisher = acm,
xvolume = 9035,
xxxseries = lncs,
mywebpage = {soft-verif},
keywords = {scala, SMT solvers},
category = {soft-verif},
show = {},
note={forthcoming},
urlpaper = {papers/scala-17.pdf},
abstract = {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.},
Type = {B - International Conferences},
show = {},
}
Downloads: 3