(Add theorem provers) |
(Explain SMT) |
||
| Line 15: | Line 15: | ||
* E | * E | ||
* prover9 (prover9-apps, prover9-devel, prover9-doc) | * prover9 (prover9-apps, prover9-devel, prover9-doc) | ||
== Satisfiability Modulo Theories (SMT) Solvers == | |||
[http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisfiability Modulo Theories (SMT) Solvers] can take a formula in first-order logic (FOL) and determine if the formula is satisfiable (e.g., if it is possible to assign variables and undefined functions/predicates so that the formulas will be true). | |||
In addition, SMT Solvers support one or more "theories", i.e., a set of predefined functions/predicates (such as those for number, lists, | |||
and so on). | |||
Many of these tools support the [http://combination.cs.uiowa.edu/smtlib/ SMT-LIB input format]. | |||
SAT solvers are often used as a building block to develop other tools. | |||
* cvc3 | |||
* alt-ergo | |||
== SAT Solvers == | == SAT Solvers == | ||
| Line 23: | Line 34: | ||
In the worst case this problem is extremely hard | In the worst case this problem is extremely hard | ||
(i.e., they are [http://en.wikipedia.org/wiki/NP-complete NP-complete]), but modern algorithms can usually solve typical SAT problems very quickly. | (i.e., they are [http://en.wikipedia.org/wiki/NP-complete NP-complete]), but modern algorithms can usually solve typical SAT problems very quickly. | ||
SAT solvers | SAT solvers are often used as a building block to develop other tools. | ||
Packages: | Packages: | ||
| Line 31: | Line 42: | ||
== Other == | == Other == | ||
The tools packaged so far, and not listed above, are: | The tools packaged so far, and not listed above, are: | ||
coq (coq-coqide, coq-doc, coq-emacs), emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO}, ppl (ppl-*), pvs-sbcl, sat4j, splint, stp (stp-devel), tex-zfuzz, why (why-coq, why-gwhy), zenon, csisat. | |||
Revision as of 15:26, 20 January 2010
Formal methods tool suite
Here are major categories of formal methods tools, along with the specific programs and packages that implement those categories in Fedora. See the Fedora Formal Methods Special Interest Group (SIG) for more information.
Theorem Provers
Theorem provers can prove whether or not a goal can be proved given a set of assumptions.
First-Order Logic (FOL) Theorem Provers
First-order Logic (FOL) is a widely-used mathematical language for stating assumptions and goals. FOL is not as expressive as some other languages, but it is sufficient for many purposes, and FOL provers tend to be able to prove much more in an automated way than those with more powerful languages (e.g., higher-order logics).
- E
- prover9 (prover9-apps, prover9-devel, prover9-doc)
Satisfiability Modulo Theories (SMT) Solvers
Satisfiability Modulo Theories (SMT) Solvers can take a formula in first-order logic (FOL) and determine if the formula is satisfiable (e.g., if it is possible to assign variables and undefined functions/predicates so that the formulas will be true). In addition, SMT Solvers support one or more "theories", i.e., a set of predefined functions/predicates (such as those for number, lists, and so on). Many of these tools support the SMT-LIB input format. SAT solvers are often used as a building block to develop other tools.
- cvc3
- alt-ergo
SAT Solvers
A SAT (satisfiability) solver can determine if boolean variables (variables which can be true or false) can have values that would make a set of formulas true. If it's possible, then the formulas are satisfiable. In the worst case this problem is extremely hard (i.e., they are NP-complete), but modern algorithms can usually solve typical SAT problems very quickly. SAT solvers are often used as a building block to develop other tools.
Packages:
- minisat2
- picosat
Other
The tools packaged so far, and not listed above, are: coq (coq-coqide, coq-doc, coq-emacs), emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO}, ppl (ppl-*), pvs-sbcl, sat4j, splint, stp (stp-devel), tex-zfuzz, why (why-coq, why-gwhy), zenon, csisat.