# Packages tagged smt

16 packages have this tag.

[Merge tag] (trustees only)Related tags: library (16), formal-methods (12), theorem-provers (12), bsd3 (10), symbolic-computation (8), math (6), gpl (5), bit-vectors (4), program (2), algorithms (1), constraints (1), deprecated (1), ...

Name |
DLs |
Rating |
Description |
Tags |
Last U/L |
Maintainer |
---|---|---|---|---|---|---|

Hsmtlib | 7 | 0.0 | Haskell library for easy interaction with SMT-LIB 2 compliant solvers. | (bsd3, library, smt) | 2014-07-02 | roger62 |

boolector | 23 | 0.0 | Haskell bindings for the Boolector SMT solver | (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers) | 2020-08-20 | DeianStefan |

hz3 (deprecated) | 9 | 0.0 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers) | 2019-10-01 | |

linearEqSolver | 5 | 0.0 | Use SMT solvers to solve linear systems over integers and rationals | (bsd3, library, math, smt) | 2020-05-13 | LeventErkok |

sbv | 2573 | 2.75 | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. | (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2021-03-30 | LeventErkok |

sbvPlugin | 163 | 0.0 | Formally prove properties of Haskell programs using SBV/SMT | (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2021-03-22 | LeventErkok |

smt2-parser | 2 | 0.0 | A Haskell parser for SMT-LIB version 2.6 | (bsd3, formal-languages, language, library, smt) | 2020-12-02 | liuyuxi |

smtLib | 20 | 0.0 | A library for working with the SMTLIB format. | (bsd3, library, smt) | 2019-01-10 | IavorDiatchki |

smtlib2 | 2 | 2.0 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-debug | 1 | 0.0 | Dump the communication with an SMT solver for debugging purposes. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-pipe | 3 | 0.0 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-quickcheck | 1 | 0.0 | Helper functions to create SMTLib expressions in QuickCheck | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-06 | HenningGuenther |

smtlib2-timing | 4 | 0.0 | Get timing informations for SMT queries | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-07 | HenningGuenther |

toysolver | 266 | 0.0 | Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc | (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers) | 2021-02-10 | MasahiroSakai |

what4 | 128 | 2.25 | Solver-agnostic symbolic values support for issuing queries | (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers) | 2021-02-09 | RobertDockins |

z3 | 13 | 2.25 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2020-08-29 | IagoAbal |