Packages tagged formal-methods

44 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (42), bsd3 (26), theorem-provers (21), smt (15), symbolic-computation (13), language (10), program (10), math (9), gpl (8), mit (8), bit-vectors (5), concurrency (5), logic (3), game (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-CoreLanguage220.04Definition of a CSP core-language. (bsd3, concurrency, formal-methods, language, library)2017-10-260.3.1.0MarcFontaine
CSPM-FiringRules160.02Firing rules semantic of CSPM (bsd3, concurrency, formal-methods, language, library)2017-10-260.4.4.0MarcFontaine
CSPM-Frontend270.04A CSP-M parser compatible with FDR-2.91 (bsd3, concurrency, formal-methods, language, library)2017-10-260.12.1.0MarcFontaine
CSPM-Interpreter230.02An interpreter for CSPM (bsd3, concurrency, formal-methods, language, library)2017-10-260.7.1.0MarcFontaine
CSPM-ToProlog160.02some modules specific for the ProB tool (bsd3, formal-methods, library)2017-10-260.5.5.0MarcFontaine
CSPM-cspm250.01cspm command line tool for analyzing CSPM specifications. (bsd3, concurrency, formal-methods, language, library, program)2017-10-260.8.1.0MarcFontaine
LPPaver50.00An automated prover targeting problems that involve nonlinear real arithmetic (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification)2023-03-130.0.5.0JunaidRasheed
PropaFP80.01Auto-active verification of floating-point programs (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers)2023-03-120.1.2.0JunaidRasheed
SmtLib40.01Library for parsing SMTLIB2 (formal-methods, library, mit)2015-02-220.1.0.0roger62
acl260.02Writing and calling ACL2 from Haskell. (bsd3, formal-methods, language, library)2014-10-010.0.1TomHawkins
afv160.01Infinite state model checking of iterative C programs. (bsd3, formal-methods, program)2010-03-310.1.1TomHawkins
atp40.00Interface to automated theorem provers (formal-methods, gpl, library, logic, math, theorem-provers)2021-01-250.1.0.0EK
boolector270.01Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-200.0.0.13DeianStefan
dove70.01The Dove verification language. (bsd3, formal-methods, language, library)2015-04-280.0.0TomHawkins
g280.01Haskell symbolic execution engine. (bsd3, formal-methods, library, program, symbolic-computation)2024-03-220.2.0.0WilliamHallahan
g2q30.00G2Q allows constraint programming, via writing Haskell predicates. (bsd3, formal-methods, library, symbolic-computation)2019-06-300.1.0.0WilliamHallahan
ghc-proofs50.01GHC plugin to prove program equations by simplification (compiler-plugin, formal-methods, library, mit)2017-09-050.1.1JoachimBreitner
grisette450.01Symbolic evaluation as a library (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-07-020.7.0.0siruilu
grisette-monad-coroutine50.00Support for monad-coroutine package with Grisette (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-01-100.2.0.0siruilu
hermit380.02Haskell Equational Reasoning Model-to-Implementation Tunnel (bsd3, formal-methods, language, library, optimization, program, refactoring, reflection, transformation)2016-02-231.0.1AndrewFarmer, AndyGill, NeilSculthorpe, ryanglscott
hz3 (deprecated)80.00Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers)2019-10-0196.0.0.0
improve600.02An imperative, verifiable programming language for high assurance applications. (bsd3, embedded, formal-methods, language, library)2011-07-290.4.0TomHawkins
opentheory280.012The standard theory library (formal-methods, library, mit)2015-07-241.200JoeHurd
opentheory-bits140.03Natural number to bit-list conversions (formal-methods, library, mit)2015-10-191.69JoeHurd
opentheory-byte150.01Bytes (formal-methods, library, mit)2015-10-191.128JoeHurd
opentheory-primitive210.013Haskell primitives used by OpenTheory packages (formal-methods, library, mit)2015-10-191.8JoeHurd
opentheory-probability140.03Probability (formal-methods, library, mit)2015-10-191.52JoeHurd
safe-coupling82.00Relational proof system for probabilistic algorithms (bsd3, formal-methods, library)2022-06-150.1.0.1oquechy
sbv3872.7512SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-05-1110.10LeventErkok
sbv-program80.00Component-based program synthesis using SBV (bit-vectors, bsd3, formal-methods, library, smt, symbolic-computation)2023-01-261.1.0.0arrowd
sbvPlugin640.01Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-05-229.10.1LeventErkok
smcdel152.00Symbolic Model Checking for Dynamic Epistemic Logic (formal-methods, gpl, library, logic, program)2024-04-241.3.0m4lvin
smtlib2172.06A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-debug40.01Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-pipe50.01A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-quickcheck50.01Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-061.0HenningGuenther
smtlib2-timing50.01Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-071.0HenningGuenther
theoremquest40.01A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)2011-02-280.0.0TomHawkins
theoremquest-client40.01A simple client for the TheoremQuest theorem proving game. (bsd3, formal-methods, game, program, theorem-provers)2011-02-280.0.0TomHawkins
toysolver600.04Assorted 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-170.8.1MasahiroSakai
tptp250.01Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-110.1.3.0EK
what4762.258Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2024-05-151.6RobertDockins, ryanglscott, galoisinc
yices-painless120.01An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)2011-01-170.1.2DonaldStewart
z3582.256Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29408.2IagoAbal