ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper)

Franck Cassez; Anthony M. Sloane

doi:10.1145/3136000.3136004

ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper)

Franck Cassez, Anthony M. Sloane

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

6 Citations (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 language	English
Title of host publication	SCALA 2017
Subtitle of host publication	Proceedings of the 8th ACM SIGPLAN International Symposium on Scala
Editors	H Miller, P Haller, O Lhotak
Place of Publication	New York, NY
Publisher	Association for Computing Machinery, Inc
Pages	51-55
Number of pages	5
ISBN (Electronic)	9781450355292
DOIs	https://doi.org/10.1145/3136000.3136004
Publication status	Published - 22 Oct 2017
Event	8th ACM SIGPLAN International Symposium on Scala, SCALA 2017 - Vancouver, Canada Duration: 22 Oct 2017 → 23 Oct 2017

Conference

Conference	8th ACM SIGPLAN International Symposium on Scala, SCALA 2017
Country/Territory	Canada
City	Vancouver
Period	22/10/17 → 23/10/17

Keywords

Logics
Scala
SMT solvers

Access to Document

10.1145/3136000.3136004

Cite this

@inproceedings{da9ef5e659b746c883fb125bf8a077bc,

title = "ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper)",

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.",

keywords = "Logics, Scala, SMT solvers",

author = "Franck Cassez and Sloane, {Anthony M.}",

year = "2017",

month = oct,

day = "22",

doi = "10.1145/3136000.3136004",

language = "English",

pages = "51--55",

editor = "H Miller and P Haller and O Lhotak",

booktitle = "SCALA 2017",

publisher = "Association for Computing Machinery, Inc",

note = "8th ACM SIGPLAN International Symposium on Scala, SCALA 2017 ; Conference date: 22-10-2017 Through 23-10-2017",

}

Cassez, F & Sloane, AM 2017, ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper). in H Miller, P Haller & O Lhotak (eds), SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala. Association for Computing Machinery, Inc, New York, NY, pp. 51-55, 8th ACM SIGPLAN International Symposium on Scala, SCALA 2017, Vancouver, Canada, 22/10/17. https://doi.org/10.1145/3136000.3136004

ScalaSMT : Satisfiability Modulo Theory in Scala (tool paper). / Cassez, Franck; Sloane, Anthony M.

SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala. ed. / H Miller; P Haller; O Lhotak. New York, NY : Association for Computing Machinery, Inc, 2017. p. 51-55.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - ScalaSMT

T2 - 8th ACM SIGPLAN International Symposium on Scala, SCALA 2017

AU - Cassez, Franck

AU - Sloane, Anthony M.

PY - 2017/10/22

Y1 - 2017/10/22

N2 - 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.

AB - 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.

KW - Logics

KW - Scala

KW - SMT solvers

UR - http://www.scopus.com/inward/record.url?scp=85037162028&partnerID=8YFLogxK

U2 - 10.1145/3136000.3136004

DO - 10.1145/3136000.3136004

M3 - Conference proceeding contribution

AN - SCOPUS:85037162028

SP - 51

EP - 55

BT - SCALA 2017

A2 - Miller, H

A2 - Haller, P

A2 - Lhotak, O

PB - Association for Computing Machinery, Inc

CY - New York, NY

Y2 - 22 October 2017 through 23 October 2017

ER -

ScalaSMT: Satisfiability Modulo Theory in Scala (tool paper)

Abstract

Conference

Keywords

Access to Document

Other files and links

Cite this