hackage.haskell.org "formal-methods" keyword
View the packages on the hackage.haskell.org package registry that are tagged with the "formal-methods" keyword.
opentheory-primitive 1.8
9 versions - Latest release: almost 10 years ago - 6.24 thousand downloads total - 1 maintainerz3 4.3.1
Bindings for the Z3 4.x Theorem Prover (https://github.com/Z3Prover/z3). Z3.Base.C provides the ...15 versions - Latest release: about 7 years ago - 16 dependent repositories - 11.2 thousand downloads total - 58 stars on GitHub - 1 maintainer
smtlib2-quickcheck 1.0
1 version - Latest release: over 8 years ago - 1 thousand downloads total - 1 maintainergrisette-monad-coroutine 0.2.0.0
Orphan instances and wrappers for monad-coroutine package with Grisette.2 versions - Latest release: over 1 year ago - 1 dependent repositories - 157 downloads total - 0 stars on GitHub - 1 maintainer
toysolver 0.9.0
Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBSPBO (Pseudo B...16 versions - Latest release: 5 months ago - 2 dependent repositories - 15.7 thousand downloads total - 157 stars on GitHub - 1 maintainer
Top 4.0% on hackage.haskell.org
128 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82 thousand downloads total - 240 stars on GitHub - 1 maintainer
sbv 0.9.24
Express properties about Haskell programs and automatically prove them using SMT (Satisfiability ...128 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82 thousand downloads total - 240 stars on GitHub - 1 maintainer
hz3 96.0.0.0 💰
Fork of z3 with future-proof version-numbering scheme Bindings for the Z3 4.x Theorem Prover (ht...1 version - Latest release: almost 6 years ago - 682 downloads total - 0 stars on GitHub
ghc-proofs 0.1.1
Often when writing Haskel code, one would like to prove things about the code. A good example is...2 versions - Latest release: almost 8 years ago - 1.64 thousand downloads total - 145 stars on GitHub - 1 maintainer
tptp 0.1.3.0
Parser and pretty printer for the TPTP language7 versions - Latest release: over 4 years ago - 1 dependent repositories - 2.52 thousand downloads total - 7 stars on GitHub - 1 maintainer
CSPM-cspm 0.8.1.0
cspm is a small command line tool for analyzing CSPM specifications.11 versions - Latest release: almost 8 years ago - 11.2 thousand downloads total - 1 maintainer
what4 1.6.3
What4 is a generic library for representing values as symbolic formulae which may contain referen...13 versions - Latest release: 5 months ago - 9 dependent packages - 18 dependent repositories - 4.84 thousand downloads total - 165 stars on GitHub - 5 maintainers
theoremquest-client 0.0.0
1 version - Latest release: over 14 years ago - 1.16 thousand downloads total - 1 maintaineryices-painless 0.1.2
3 versions - Latest release: over 14 years ago - 2.55 thousand downloads total - 1 maintainergrisette 0.13.0.1
Grisette is a reusable symbolic evaluation library for Haskell. By translating programs into cons...18 versions - Latest release: 13 days ago - 1 dependent package - 2 dependent repositories - 844 downloads total - 67 stars on GitHub - 1 maintainer
CSPM-Interpreter 0.7.1.0
This package contains an interpreter for CSPM and instance declarations that implement the interf...11 versions - Latest release: almost 8 years ago - 11.1 thousand downloads total - 1 maintainer
CSPM-CoreLanguage 0.3.1.0
This package contains an interface for the CSP core-language. It defines processes, events, event...8 versions - Latest release: almost 8 years ago - 8.47 thousand downloads total - 1 maintainer
opentheory-byte 1.128
5 versions - Latest release: almost 10 years ago - 3.37 thousand downloads total - 1 maintainerCSPM-Frontend 0.12.1.0
CSP-M is the machine readable syntax of CSP (concurrent sequential processes) as used by the form...13 versions - Latest release: almost 8 years ago - 1 dependent repositories - 13.1 thousand downloads total - 1 maintainer
CSPM-ToProlog 0.5.5.0
This package contains a translation from a CSPM AST to the representation used by the ProB tool. ...6 versions - Latest release: almost 8 years ago - 1 dependent repositories - 5.96 thousand downloads total - 1 maintainer
g2 0.2.0.0
A Haskell symbolic execution engine. For details, please see: https://github.com/BillHallahan/G23 versions - Latest release: over 1 year ago - 1 dependent package - 2 dependent repositories - 997 downloads total - 1 maintainer
hermit 1.0.1
HERMIT is a Haskell-specific toolkit designed to mechanize equational reasoning and program trans...18 versions - Latest release: over 9 years ago - 6 dependent repositories - 17.3 thousand downloads total - 4 maintainers
theoremquest 0.0.0
1 version - Latest release: over 14 years ago - 1 dependent repositories - 1.2 thousand downloads total - 1 maintainersmtlib2 0.3.1
5 versions - Latest release: about 9 years ago - 1 dependent package - 4 dependent repositories - 4.46 thousand downloads total - 1 maintainerLPPaver 0.0.5.0
Please see the README on GitHub at https://github.com/rasheedja/LPPaver#readme2 versions - Latest release: over 2 years ago - 1 dependent package - 1 dependent repositories - 166 downloads total - 5 stars on GitHub - 1 maintainer
SmtLib 0.1.0.0
Parser for smt-lib Command responses1 version - Latest release: over 10 years ago - 1.22 thousand downloads total - 2 stars on GitHub - 1 maintainer
smtlib2-timing 1.0
1 version - Latest release: over 8 years ago - 1.02 thousand downloads total - 1 maintaineropentheory-bits 1.69
5 versions - Latest release: almost 10 years ago - 3.31 thousand downloads total - 1 maintainersafe-coupling 0.1.0.1
Relational proof system for probabilistic algorithms. Supports two proving methods: upper bound K...2 versions - Latest release: about 3 years ago - 1 dependent repositories - 188 downloads total - 3 stars on GitHub - 1 maintainer
smtlib2-pipe 1.0
1 version - Latest release: over 8 years ago - 1 dependent repositories - 1.08 thousand downloads total - 1 maintaineracl2 0.0.1
2 versions - Latest release: almost 11 years ago - 2.45 thousand downloads total - 1 maintainerCSPM-FiringRules 0.4.4.0
This package contains functions for computing the transitions of a CSP process based on the stand...7 versions - Latest release: almost 8 years ago - 7.47 thousand downloads total - 1 maintainer
sbv-program 1.1.0.0
Given a library of available componen functions, synthesize a program implementing a specification.2 versions - Latest release: over 2 years ago - 1 dependent repositories - 159 downloads total - 0 stars on GitHub - 1 maintainer
afv 0.1.1
7 versions - Latest release: over 15 years ago - 5.84 thousand downloads total - 1 maintainerimprove 0.4.0
An imperative programming language in Haskell for high assurance embedded applications. ImProve ...29 versions - Latest release: almost 14 years ago - 20.4 thousand downloads total - 57 stars on GitHub - 1 maintainer
dove 0.0.0
1 version - Latest release: about 10 years ago - 1.11 thousand downloads total - 1 maintainerPropaFP 0.1.2.0
Please see the README on GitHub at https://github.com/rasheedja/PropaFP#readme3 versions - Latest release: over 2 years ago - 2 dependent packages - 2 dependent repositories - 238 downloads total - 8 stars on GitHub - 1 maintainer
sbvPlugin 9.12.1
GHC plugin for proving properties over Haskell functions using SMT solvers, based on the SBV pack...20 versions - Latest release: 5 months ago - 1 dependent repositories - 6.68 thousand downloads total - 45 stars on GitHub - 1 maintainer
opentheory 1.200
9 versions - Latest release: about 10 years ago - 6.31 thousand downloads total - 1 maintaineratp 0.1.0.0
Haskell interface to automated theorem provers1 version - Latest release: over 4 years ago - 1 dependent repositories - 223 downloads total - 9 stars on GitHub - 1 maintainer
opentheory-probability 1.52
5 versions - Latest release: almost 10 years ago - 3.49 thousand downloads total - 1 maintainerboolector 0.0.0.13
Haskell bindings for the Boolector SMT solver13 versions - Latest release: almost 5 years ago - 2 dependent repositories - 6.16 thousand downloads total - 5 stars on GitHub - 1 maintainer
g2q 0.1.0.0
G2Q allows constraint programming, via writing Haskell predicates. A quasiquoter, g2, is provided...1 version - Latest release: about 6 years ago - 533 downloads total - 1 maintainer
smtlib2-debug 1.0
1 version - Latest release: over 8 years ago - 1 dependent repositories - 1.02 thousand downloads total - 1 maintainer
Related Keywords
Propose Tags
43
library
41
bsd3
26
theorem-provers
21
smt
15
symbolic-computation
13
language
10
math
9
program
9
haskell
8
mit
8
gpl
7
bit-vectors
5
concurrency
5
verification
4
theorem-prover
3
theorem-proving
3
logic
3
optimization
2
tptp
2
game
2
mpl
2
maths
2
mathematics
2
automated-theorem-provers
2
synthesis
1
refactoring
1
symbolic-execution
1
reflection
1
api
1
transformation
1
automatic-theorem-proving
1
embedded
1
floating-point
1
floating-point-arithmetic
1
formal-verification
1
sbv
1
atp
1
first-order-logic
1
prover
1
z3
1
algorithms
1
constraints
1
optimisation
1
mathematical-programming
1
sat-solver
1
smt-solver
1
deprecated
1
compiler-plugin
1
parsing
1
pretty-printer
1
eprover
1
haskell-library
1
parsing-library
1
pretty-print
1
vampire
1
symbolic-evaluation
1