Journal
VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, VSTTE 2016
Volume 9971, Issue -, Pages 139-148Publisher
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-319-48869-1_11
Keywords
-
Ask authors/readers for more resources
Satisfiability Modulo Theory (SMT) solvers received a lot of attention in the research community in the last decade, and consequently their expressiveness and performance have significantly improved. In the areas of program analysis and model checking, many of the newly developed tools rely on SMT solving. The SMT-LIB initiative defines a common format for communication with an SMT solver. However, tool developers often prefer to use the solver API instead, because many features offered by SMT solvers such as interpolation, optimization, and formula introspection are not supported by SMT-LIB directly. Additionally, using SMT-LIB for communication incurs a performance overhead, because all the queries to the solver have to be serialized to strings. Yet using the API directly creates the problem of a solver lock-in, which makes evaluating a tool with different solvers very difficult. We present JavaSMT, a library that exposes a solver-independent API layer for SMT solving. Our library aims to close the gap between API-based and SMT-LIB-based communication, by offering a large set of features with minimal performance overhead. JavaSMT has been used internally in CPACHECKER since inception, and has been heavily tested in different verification algorithms.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available