ScalaSMT

Satisfiability Modulo Theory in Scala (tool paper)

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

1 Citation (Scopus)

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.

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

Conference

Conference8th ACM SIGPLAN International Symposium on Scala, SCALA 2017
CountryCanada
CityVancouver
Period22/10/1723/10/17

Keywords

  • Logics
  • Scala
  • SMT solvers

Cite this

Cassez, F., & Sloane, A. M. (2017). ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper). In SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala (pp. 51-55). New York, NY: Association for Computing Machinery, Inc. https://doi.org/10.1145/3136000.3136004