jSMTLIB: Tutorial, validation and adapter tools for SMT-LIBv2. The SMT-LIB standard defines an input format and response requirements for Satisfiability-Modulo-Theories automated reasoning tools. The standard has been an incentive to improving and comparing the increasing supply of SMT solvers. It could also be more widely used in applications, providing a uniform interface and portability across different SMT tools. This tool paper describes a tutorial and accompanying software package, jSMTLIB, that will help users of SMT solvers understand and apply the newly revised SMT-LIB format; the tutorial also describes fine points of the SMT-LIB format which, along with a compliance suite, will be useful to SMT implementors. Finally, the tool suite includes adapters that allow using some older solvers, such as Simplify, as SMT-LIB compliant tools.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 2 articles , 1 standard article )

Showing results 1 to 2 of 2.
Sorted by year (citations)

  1. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  2. Cok, David R.: jSMTLIB: Tutorial, validation and adapter tools for SMT-LIBv2 (2011) ioport