Packages tagged formal-methods
43 packages have this tag.
[Merge tag] (trustees only)Related tags: library (41), bsd3 (26), theorem-provers (21), smt (15), symbolic-computation (13), language (10), math (9), program (9), mit (8), gpl (7), bit-vectors (5), concurrency (5), game (2), logic (2), mathematics (2), maths (2), mpl (2), optimization (2), algorithms (1), compiler-plugin (1), ...
Name |
DLs |
Rating |
Rev Deps |
Description |
Tags |
Last U/L |
Last Version |
Maintainers |
|---|---|---|---|---|---|---|---|---|
| CSPM-CoreLanguage | 15 | 0.0 | 4 | Definition of a CSP core-language. | (bsd3, concurrency, formal-methods, language, library) | 2017-10-26 | 0.3.1.0 | MarcFontaine |
| CSPM-FiringRules | 2 | 0.0 | 2 | Firing rules semantic of CSPM | (bsd3, concurrency, formal-methods, language, library) | 2017-10-26 | 0.4.4.0 | MarcFontaine |
| CSPM-Frontend | 1 | 0.0 | 4 | A CSP-M parser compatible with FDR-2.91 | (bsd3, concurrency, formal-methods, language, library) | 2017-10-26 | 0.12.1.0 | MarcFontaine |
| CSPM-Interpreter | 3 | 0.0 | 2 | An interpreter for CSPM | (bsd3, concurrency, formal-methods, language, library) | 2017-10-26 | 0.7.1.0 | MarcFontaine |
| CSPM-ToProlog | 8 | 0.0 | 2 | some modules specific for the ProB tool | (bsd3, formal-methods, library) | 2017-10-26 | 0.5.5.0 | MarcFontaine |
| CSPM-cspm | 1 | 0.0 | 1 | cspm command line tool for analyzing CSPM specifications. | (bsd3, concurrency, formal-methods, language, library, program) | 2017-10-26 | 0.8.1.0 | MarcFontaine |
| LPPaver | 2 | 0.0 | 0 | An automated prover targeting problems that involve nonlinear real arithmetic | (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification) | 2023-03-13 | 0.0.5.0 | JunaidRasheed |
| PropaFP | 5 | 0.0 | 1 | Auto-active verification of floating-point programs | (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers) | 2023-03-12 | 0.1.2.0 | JunaidRasheed |
| SmtLib | 0 | 0.0 | 1 | Library for parsing SMTLIB2 | (formal-methods, library, mit) | 2015-02-22 | 0.1.0.0 | roger62 |
| acl2 | 1 | 0.0 | 2 | Writing and calling ACL2 from Haskell. | (bsd3, formal-methods, language, library) | 2014-10-01 | 0.0.1 | TomHawkins |
| afv | 4 | 0.0 | 1 | Infinite state model checking of iterative C programs. | (bsd3, formal-methods, program) | 2010-03-31 | 0.1.1 | TomHawkins |
| atp | 1 | 0.0 | 0 | Interface to automated theorem provers | (formal-methods, gpl, library, logic, math, theorem-provers) | 2021-01-25 | 0.1.0.0 | EK |
| boolector | 2 | 0.0 | 1 | Haskell bindings for the Boolector SMT solver | (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers) | 2020-08-20 | 0.0.0.13 | DeianStefan |
| dove | 0 | 0.0 | 1 | The Dove verification language. | (bsd3, formal-methods, language, library) | 2015-04-28 | 0.0.0 | TomHawkins |
| g2 | 3 | 0.0 | 1 | Haskell symbolic execution engine. | (bsd3, formal-methods, library, program, symbolic-computation) | 2019-06-30 | 0.1.0.1 | WilliamHallahan |
| g2q | 1 | 0.0 | 0 | G2Q allows constraint programming, via writing Haskell predicates. | (bsd3, formal-methods, library, symbolic-computation) | 2019-06-30 | 0.1.0.0 | WilliamHallahan |
| ghc-proofs | 1 | 0.0 | 1 | GHC plugin to prove program equations by simplification | (compiler-plugin, formal-methods, library, mit) | 2017-09-05 | 0.1.1 | JoachimBreitner |
| grisette | 7 | 0.0 | 1 | Symbolic evaluation as a library | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2023-09-29 | 0.3.1.1 | siruilu |
| grisette-monad-coroutine | 1 | 0.0 | 0 | Support for monad-coroutine package with Grisette | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2023-02-03 | 0.1.0.0 | siruilu |
| hermit | 7 | 0.0 | 2 | Haskell Equational Reasoning Model-to-Implementation Tunnel | (bsd3, formal-methods, language, library, optimization, program, refactoring, reflection, transformation) | 2016-02-23 | 1.0.1 | AndrewFarmer, AndyGill, NeilSculthorpe, ryanglscott |
| hz3 (deprecated) | 3 | 0.0 | 0 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers) | 2019-10-01 | 96.0.0.0 | |
| improve | 13 | 0.0 | 2 | An imperative, verifiable programming language for high assurance applications. | (bsd3, embedded, formal-methods, language, library) | 2011-07-29 | 0.4.0 | TomHawkins |
| opentheory | 14 | 0.0 | 12 | The standard theory library | (formal-methods, library, mit) | 2015-07-24 | 1.200 | JoeHurd |
| opentheory-bits | 3 | 0.0 | 3 | Natural number to bit-list conversions | (formal-methods, library, mit) | 2015-10-19 | 1.69 | JoeHurd |
| opentheory-byte | 1 | 0.0 | 1 | Bytes | (formal-methods, library, mit) | 2015-10-19 | 1.128 | JoeHurd |
| opentheory-primitive | 2 | 0.0 | 13 | Haskell primitives used by OpenTheory packages | (formal-methods, library, mit) | 2015-10-19 | 1.8 | JoeHurd |
| opentheory-probability | 3 | 0.0 | 3 | Probability | (formal-methods, library, mit) | 2015-10-19 | 1.52 | JoeHurd |
| safe-coupling | 1 | 2.0 | 0 | Relational proof system for probabilistic algorithms | (bsd3, formal-methods, library) | 2022-06-15 | 0.1.0.1 | oquechy |
| sbv | 206 | 2.75 | 12 | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. | (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2023-06-09 | 10.2 | LeventErkok |
| sbv-program | 3 | 0.0 | 0 | Component-based program synthesis using SBV | (bit-vectors, bsd3, formal-methods, library, smt, symbolic-computation) | 2023-01-26 | 1.1.0.0 | arrowd |
| sbvPlugin | 6 | 0.0 | 1 | Formally prove properties of Haskell programs using SBV/SMT | (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2023-04-14 | 9.6.1 | LeventErkok |
| smtlib2 | 1 | 2.0 | 6 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-debug | 0 | 0.0 | 1 | Dump the communication with an SMT solver for debugging purposes. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-pipe | 1 | 0.0 | 1 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-quickcheck | 1 | 0.0 | 1 | Helper functions to create SMTLib expressions in QuickCheck | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-06 | 1.0 | HenningGuenther |
| smtlib2-timing | 3 | 0.0 | 1 | Get timing informations for SMT queries | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-07 | 1.0 | HenningGuenther |
| theoremquest | 0 | 0.0 | 1 | A common library for TheoremQuest, a theorem proving game. | (bsd3, formal-methods, game, library, theorem-provers) | 2011-02-28 | 0.0.0 | TomHawkins |
| theoremquest-client | 1 | 0.0 | 1 | A simple client for the TheoremQuest theorem proving game. | (bsd3, formal-methods, game, program, theorem-provers) | 2011-02-28 | 0.0.0 | TomHawkins |
| toysolver | 10 | 0.0 | 4 | Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc | (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers) | 2022-09-17 | 0.8.1 | MasahiroSakai |
| tptp | 0 | 0.0 | 1 | Parser and pretty printer for the TPTP language | (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers) | 2021-01-11 | 0.1.3.0 | EK |
| what4 | 68 | 2.25 | 2 | Solver-agnostic symbolic values support for issuing queries | (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers) | 2023-07-31 | 1.5 | RobertDockins, ryanglscott, galoisinc |
| yices-painless | 1 | 0.0 | 1 | An embedded language for programming the Yices SMT solver | (bsd3, formal-methods, library, math, theorem-provers) | 2011-01-17 | 0.1.2 | DonaldStewart |
| z3 | 24 | 2.25 | 6 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2020-08-29 | 408.2 | IagoAbal |