ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper)

Franck Cassez, Anthony M. Sloane

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

6 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationSCALA 2017
Subtitle of host publicationProceedings of the 8th ACM SIGPLAN International Symposium on Scala
EditorsH Miller, P Haller, O Lhotak
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery, Inc
Number of pages5
ISBN (Electronic)9781450355292
Publication statusPublished - 22 Oct 2017
Event8th ACM SIGPLAN International Symposium on Scala, SCALA 2017 - Vancouver, Canada
Duration: 22 Oct 201723 Oct 2017


Conference8th ACM SIGPLAN International Symposium on Scala, SCALA 2017


  • Logics
  • Scala
  • SMT solvers

Cite this