« zurück

metaSMT - An Embedded Domain Specific Language for SMT

Abstract
metaSMT provides an easy to use Embedded Domain Specific Language (EDSL) for C++ similar to SMT-LIB. Various Satisfiability (SAT) and SAT Modulo Theories (SMT) solvers can be used directly over their API through the language. The main advantages of metaSMT are:

• Engine independence through efficient abstraction layers
• Simplified development of algorithms based on formal methods
• Extensibility in terms of input language and reasoning engines
• Customizability in terms of optimization and infrastructure
• Translation of the input language into native engine calls at compile time

Features

• Theories and logics:
  • Simple Boolean expressions over Boolean predicates
  • Closed quantifier-free formulas over the theory of fixed-size bit-vectors (QF_BV)
  • Closed quantifier-free formulas over the theory of bit-vectors and bit-vector arrays (QF_ABV)
• Assertion management:
  • Stack with push and pop (as in SMT-LIB 2.0)
  • Groups of assertions (creation, deletion)
  • Assumptions (valid during one SAT call)
• Supported SMT solvers: Boolector, Z3, STP SWORD
• Supported SAT solvers: MiniSAT (API), PicoSAT (API), Glucose (CNF files), PrecoSAT (CNF files), Plingeling (CNF files)
• Other: CUDD, Aiger

Download  [Changes]

• metaSMT Version 3, from November 2011
  metaSMT-3.tar.gz (source)
• metaSMT Version 2, from June 2011
  >metaSMT-2.tar.gz (source)
• metaSMT Version 1, from June 2011
  metaSMT-1.tar.gz (source)

Development
Since June 2012 the metaSMT project is developed on GitHub: metaSMT GitHub project. Dependency scripts are available on GitHub (dependencies GitHub), too.

License
metaSMT is published under MIT license as contained in the source archive.

Contact
Please contact Rolf Drechsler in case of questions and/or problems at drechsler@uni-bremen.de.

References

• [RHF+:2016] Heinz Riener, Finn Haedicke, Stefan Frehse, Mathias Soeken, Daniel Große, Rolf Drechsler, Görschwin Fey: "metaSMT: Focus On Your Application And Not On Solver Integration", International Journal of Software Tools for Technology Transfer (STTT), 2016. DOI10.1007/s10009-016-0426-1.
• [RSW+:2014] Heinz Riener, Mathias Soeken, Clemens Werther, Görschwin Fey, and Rolf Drechsler: "metaSMT: A Unified Interface to SMT-LIB2", Forum on specification & Design Languages (FDL), 2014.
  Download Paper | Download Slides | Benchmarks
• [RKD+:2014] Heinz Riener, Oliver Keszöcze, Rolf Drechsler, Görschwin Fey, "A Logic for Cardinality Constraints", 17. ITG/GMM/GI-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'14), Böblingen, Germany, 2014.
  
• [HFF+:2011] Finn Haedicke, Stefan Frehse, Görschwin Fey, Daniel Große, and Rolf Drechsler: "metaSMT: Focus On Your Application Not On Solver Integration", First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), 2011.
  Download Paper | Download Slides

Users of metaSMT

• metaSMT is used in metaSMT-webifc, a portfolio solver with a web-based input interface. A variety of different decision procedures are provided which solve a given SMT instance, optionally in parallel.
• metaSMT is used for constraint random verification of SystemC models. For more details see www.systemc-verification.org
• metaSMT is used by the Software Reliability Group at Imperial College London for symbolic execution supporting multiple SMT solvers.