Packages tagged formal-methods

41 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (39), bsd3 (23), theorem-provers (19), smt (12), symbolic-computation (11), language (10), program (10), math (9), gpl (8), mit (8), concurrency (5), bit-vectors (4), logic (3), game (2), mathematics (2), maths (2), mpl (2), optimization (2), algorithms (1), compiler-plugin (1), ...

Name
DLs
Rating
Description
Tags
Last U/L
Maintainer
CSPM-CoreLanguage220.0Definition of a CSP core-language. (bsd3, concurrency, formal-methods, language, library)2017-10-26MarcFontaine
CSPM-FiringRules240.0Firing rules semantic of CSPM (bsd3, concurrency, formal-methods, language, library)2017-10-26MarcFontaine
CSPM-Frontend300.0A CSP-M parser compatible with FDR-2.91 (bsd3, concurrency, formal-methods, language, library)2017-10-26MarcFontaine
CSPM-Interpreter310.0An interpreter for CSPM (bsd3, concurrency, formal-methods, language, library)2017-10-26MarcFontaine
CSPM-ToProlog120.0some modules specific for the ProB tool (bsd3, formal-methods, library)2017-10-26MarcFontaine
CSPM-cspm280.0cspm command line tool for analyzing CSPM specifications. (bsd3, concurrency, formal-methods, language, library, program)2017-10-26MarcFontaine
LPPaver00.0An automated prover targeting problems that involve nonlinear real arithmetic (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification)2022-10-26JunaidRasheed
PropaFP40.0Auto-active verification of floating-point programs (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers)2022-10-13JunaidRasheed
SmtLib30.0Library for parsing SMTLIB2 (formal-methods, library, mit)2015-02-22roger62
acl250.0Writing and calling ACL2 from Haskell. (bsd3, formal-methods, language, library)2014-10-01TomHawkins
afv120.0Infinite state model checking of iterative C programs. (bsd3, formal-methods, program)2010-03-31TomHawkins
atp30.0Interface to automated theorem provers (formal-methods, gpl, library, logic, math, theorem-provers)2021-01-25EK
boolector270.0Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-20DeianStefan
dove40.0The Dove verification language. (bsd3, formal-methods, language, library)2015-04-28TomHawkins
g230.0Haskell symbolic execution engine. (bsd3, formal-methods, library, program, symbolic-computation)2019-06-30WilliamHallahan
g2q20.0G2Q allows constraint programming, via writing Haskell predicates. (bsd3, formal-methods, library, symbolic-computation)2019-06-30WilliamHallahan
ghc-proofs30.0GHC plugin to prove program equations by simplification (compiler-plugin, formal-methods, library, mit)2017-09-05JoachimBreitner
hermit180.0Haskell Equational Reasoning Model-to-Implementation Tunnel (bsd3, formal-methods, language, library, optimization, program, refactoring, reflection, transformation)2016-02-23AndrewFarmer, AndyGill, NeilSculthorpe, ryanglscott
hz3 (deprecated)20.0Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers)2019-10-01
improve320.0An imperative, verifiable programming language for high assurance applications. (bsd3, embedded, formal-methods, language, library)2011-07-29TomHawkins
opentheory110.0The standard theory library (formal-methods, library, mit)2015-07-24JoeHurd
opentheory-bits50.0Natural number to bit-list conversions (formal-methods, library, mit)2015-10-19JoeHurd
opentheory-byte90.0Bytes (formal-methods, library, mit)2015-10-19JoeHurd
opentheory-primitive140.0Haskell primitives used by OpenTheory packages (formal-methods, library, mit)2015-10-19JoeHurd
opentheory-probability50.0Probability (formal-methods, library, mit)2015-10-19JoeHurd
safe-coupling22.0Relational proof system for probabilistic algorithms (bsd3, formal-methods, library)2022-06-15oquechy
sbv2942.75SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2022-04-27LeventErkok
sbvPlugin160.0Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2022-04-27LeventErkok
smcdel100.0Symbolic Model Checking for Dynamic Epistemic Logic (formal-methods, gpl, library, logic, program, symbolic-computation)2022-02-22m4lvin
smtlib272.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-debug40.0Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-pipe40.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-quickcheck40.0Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-06HenningGuenther
smtlib2-timing10.0Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-07HenningGuenther
theoremquest10.0A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)2011-02-28TomHawkins
theoremquest-client20.0A simple client for the TheoremQuest theorem proving game. (bsd3, formal-methods, game, program, theorem-provers)2011-02-28TomHawkins
toysolver310.0Assorted 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-17MasahiroSakai
tptp00.0Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-11EK
what4442.25Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2022-04-19RobertDockins, ryanglscott, galoisinc
yices-painless50.0An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)2011-01-17DonaldStewart
z3632.25Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29IagoAbal