- Bitwuzla + veriT SMT Solver
-Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point …
- -From fb51f11cd44675e061e494d500ee43d2ded7a76a Mon Sep 17 00:00:00 2001
From: Landon Taylor Formal Methods Tools
@@ -74,6 +82,7 @@
diff --git a/about/index.html b/about/index.html
index 43d0164..9c1ce0b 100644
--- a/about/index.html
+++ b/about/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -35,6 +35,14 @@
+
+
+
+
Formal Methods Tools
@@ -78,9 +86,9 @@
This is one of my hobby projects.
I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online.
I wanted to solve this problem, so I have been chipping away at this website for a while now.
I love to collaborate, either on this website or on any of my other formal methods projects. Please feel free to reach out if you want to talk.
+I love to collaborate, either on this website or on any of my other formal methods projects. Please feel free to reach out if you want to talk.
I welcome contributions from anyone interested in formal methods. Add tools you love or maintain, report issues, or fix a typo. Learn more on the Contribute page.
+I welcome contributions from anyone interested in formal methods. Add tools you love or maintain, report issues, or fix a typo. Learn more on the Contribute page.
@@ -91,6 +99,7 @@ I wanted to solve this problem, so I have been chipping away at this website for diff --git a/applications/constraint-solver/index.html b/applications/constraint-solver/index.html index 5f4733b..b124272 100644 --- a/applications/constraint-solver/index.html +++ b/applications/constraint-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -35,6 +35,14 @@ + + + +Contribute | About | License | Privacy
+© Copyright 2025. An open-source project.
diff --git a/applications/index.xml b/applications/index.xml index 56f8230..d08929c 100644 --- a/applications/index.xml +++ b/applications/index.xml @@ -2,38 +2,52 @@Tool | + +Description | + +
---|---|
Sally | +Sally is a model checker for infinite state systems described as transition systems. + | + + + +
Tool | + +Description | + +
---|---|
PRISM | +PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that … | + + + +
STAMINA | +A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces … | + + + +
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.
+Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.
Tool | + +Description | + +
---|---|
PRISM | +PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that … | + + + +
Tool | + +Description | + +
---|---|
STAMINA | +A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces … | + + + +
Welcome to this collection of Formal Methods Tools, which aims to be the world’s most comprehensive source for information on tools for formal methods. From decades-old classics to cutting-edge tools, this site aims to put as much information as possible into one convenient place. -Explore a wide selection of tools, contribute tools you make or love, and help grow the formal methods community.
+Explore a wide selection of tools, contribute tools you make or love, and help grow the formal methods community.Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site).
-
+
-SMT Solvers
+List of Tools
-
+
-Model Checkers
+Taxonomy Data
@@ -95,37 +103,13 @@ Contribute
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point … Colibri is an SMT solver.
- cvc5 is an automatic theorem prover for SMT problems.
- veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal … [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.
- [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and … [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … [ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers … SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
-APIs and Bindings This tool is … ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in … veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal … Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
-APIs and Bindings This tool is available … [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5
- Lingeling is a SAT solver.
- STP is a constraint solver for quantifier-free bitvectors.
-APIs and Bindings This tool is available through the following … SMT-RAT is an SMT Real Algebra Toolbox.
+APIs and Bindings This tool is available through the following interfaces:
+C++ API: … Colibri is an SMT solver.
+
- Bitwuzla
+ veriT
SMT Solver
-
- Colibri
-
- SMT Solver
-
-
-
- cvc5
-
- Theorem Prover
-
-
-
- Q3B
+ SMT-RAT
- SMT Solver
+ SMT Toolbox
-
- MiniSat
-
- SAT Solver
-
-
-
- Boolector
-
- SMT Solver
-
-
-
- MathSAT
-
- SMT Solver
-
-
-
- SMTInterpol
-
- Interpolating SMT Solver
-
-
-
- ParaFROST
-
- SMT Solver
-
-
-
- veriT
-
- SMT Solver
-
-
-
- Z3
-
- Theorem Prover
-
-
-
- cvc4
-
- Theorem Prover
-
-
-
- Lingeling
-
- SMT Solver
-
-
-
- STP
-
- Simple Theorem Prover
-
-
-
+ Colibri
+
+ SMT Solver
+
+
+
Riss
@@ -290,6 +172,109 @@ APIs and Bindings This tool is available through the following …
A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM. …
+ STAMINA +ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in …
+ ParaFROST +[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …
+ MiniSat +OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand …
+ OpenSMT +Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. +APIs and Bindings This tool is available …
+ Z3 +[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs. +
+ Q3B +STP is a constraint solver for quantifier-free bitvectors. +APIs and Bindings This tool is available through the following …
+ STP +[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5 +
+ cvc4 +[ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers …
+ MathSAT +[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as …
- dReal +cvc5 is an automatic theorem prover for SMT problems. +
+ cvc5SMT-RAT is an SMT Real Algebra Toolbox. -APIs and Bindings This tool is available through the following interfaces: -C++ API: …
- SMT-RAT +[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …
+ Boolector +SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. +APIs and Bindings This tool is …
+ SMTInterpol +PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or …
+ PRISMTool | + +Description | + +
---|---|
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Tool | + +Description | + +
---|---|
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Contribute | About | License | Privacy
+© Copyright 2025. An open-source project.
diff --git a/inputs/index.xml b/inputs/index.xml index d5f9346..d5b0723 100644 --- a/inputs/index.xml +++ b/inputs/index.xml @@ -2,38 +2,87 @@Tool | + +Description | + +
---|---|
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Tool | + +Description | + +
---|---|
PRISM | +PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that … | + + + +
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Tool | + +Description | + +
---|---|
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Tool | + +Description | + +
---|---|
PRISM | +PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that … | + + + +
STAMINA | +A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces … | + + + +
Storm | +Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + | + + + +
Tool | + +Description | + +
---|---|
Sally | +Sally is a model checker for infinite state systems described as transition systems. + | + + + +
This page lists all of the model checking tools on this site in alphabetical order. +Click a tool name in the first column to view tool details. +Click a colorful item in the second column to view all the tools for which that term applies. +Item colors mean nothing and are intended to make it easy to skim the page. +Colors are generated by hashing each term’s name and converting it to RGB color values.
+ +Tool | +Applications | +Licenses | + + +
---|---|---|
+ + + Sally + + + | ++ + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + | ++ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + + + | + + +
+ + Applications + + | ++ + + + + + + + + + + Model Checker + + + + | +
+ + Developers + + | ++ + + + + + + + + + + SRI International + + + + | +
+ + Inputs + + | ++ + + + + + + + + + + Sally + + + + | +
+ + Interfaces + + | ++ + + + + + + + + + + CLI + + + + | +
+ + Licenses + + | ++ + + + + + + + + + + GPLv2 + + + + | +
+ + Maintenance + + | ++ + + + + + + + + + + Actively Maintained + + + + | +
Sally is a model checker for infinite state systems described as transition systems.
+ +This page lists all of the SAT & SMT tools on this site in alphabetical order. -Click a tool name in the first column to view tool details. -Click a colorful item in the second column to view all the tools for which that term applies. -Item colors mean nothing and are intended to make it easy to skim the page. -Colors are generated by hashing each term’s name and converting it to RGB color values.
- -Tool | -Applications | -License | - -
---|
This page lists all of the probabilistic tools on this site in alphabetical order. +Click a tool name in the first column to view tool details. +Click a colorful item in the second column to view all the tools for which that term applies. +Item colors mean nothing and are intended to make it easy to skim the page. +Colors are generated by hashing each term’s name and converting it to RGB color values.
+ +Tool | +Applications | +Licenses | + + +
---|---|---|
+ + + PRISM + + + | ++ + + + + + + + + + + + + + + Probabilistic Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + | ++ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + + + + + | + + +
+ + + STAMINA + + + | ++ + + + + + + + + + + + + + + Probabilistic Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + | ++ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + | + + +
+ + + Storm + + + | ++ + + + + + + + + + + + + + + Probabilistic Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + | ++ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + | + + +
+ + Applications + + | ++ + + + + + + + + + + Probabilistic Model Checker + + + + | +
+ + Developers + + | ++ + + + + + + + + + + Oxford University + + + + | +
+ + Inputs + + | ++ + + + + + + + + + + MRMC + + + + + + + + + + + + + PRISM + + + + | +
+ + Interfaces + + | ++ + + + + + + + + + + CLI + + + + + + + + + + + + + Java + + + + | +
+ + Licenses + + | ++ + + + + + + + + + + GPLv2 + + + + | +
+ + Maintenance + + | ++ + + + + + + + + + + Actively Maintained + + + + | +
PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.
+ ++ + Applications + + | ++ + + + + + + + + + + Probabilistic Model Checker + + + + | +
+ + Developers + + | ++ + + + + + + + + + + Utah State University + + + + | +
+ + Inputs + + | ++ + + + + + + + + + + PRISM + + + + | +
+ + Interfaces + + | ++ + + + + + + + + + + CLI + + + + + + + + + + + + + Online + + + + | +
+ + Licenses + + | ++ + + + + + + + + + + GPLv3 + + + + + + + + + + + + + MIT + + + + | +
+ + Maintenance + + | ++ + + + + + + + + + + Actively Maintained + + + + | +
A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM.
+ ++ + Applications + + | ++ + + + + + + + + + + Probabilistic Model Checker + + + + | +
+ + Developers + + | ++ + + + + + + + + + + RWTH Aachen + + + + | +
+ + Inputs + + | ++ + + + + + + + + + + Galileo + + + + + + + + + + + + + GreatSPN + + + + + + + + + + + + + JANI + + + + + + + + + + + + + MRMC + + + + + + + + + + + + + PNML + + + + + + + + + + + + + PRISM + + + + | +
+ + Interfaces + + | ++ + + + + + + + + + + C++ + + + + + + + + + + + + + CLI + + + + + + + + + + + + + Python + + + + | +
+ + Licenses + + | ++ + + + + + + + + + + GPLv3 + + + + | +
+ + Maintenance + + | ++ + + + + + + + + + + Actively Maintained + + + + | +
Storm is a tool for the analysis of systems involving random or probabilistic phenomena.
+ +