JavaSMT: A Unified Interface for SMT Solvers in Java
| Autor: | Dirk Beyer, Egor George Karpenkov, Karlheinz Friedberger |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Java Programming language Computer science 020207 software engineering 02 engineering and technology Parallel computing Solver computer.software_genre CPAchecker Satisfiability Program analysis Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering Overhead (computing) 020201 artificial intelligence & image processing computer computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319488684 VSTTE |
| DOI: | 10.1007/978-3-319-48869-1_11 |
| Popis: | 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. The library is available from its Github website https://github.com/sosy-lab/java-smt. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|