(Initial version) |
(Add "SAT Solver" category) |
||
| Line 6: | Line 6: | ||
for more information. | for more information. | ||
The tools packaged so far are: | == SAT Solvers == | ||
E, alt-ergo, coq (coq-coqide, coq-doc, coq-emacs), cvc3, emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO} | A [http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 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 [http://en.wikipedia.org/wiki/NP-complete NP-complete]), but modern algorithms can usually solve typical SAT problems very quickly. | |||
SAT solvers aren't usually used directly by people; instead, they are a building block used by many other tools. | |||
Packages: | |||
* minisat2 | |||
* picosat | |||
== Other == | |||
The tools packaged so far, and not listed above, are: | |||
E, alt-ergo, coq (coq-coqide, coq-doc, coq-emacs), cvc3, emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO}, ppl (ppl-*), prover9 (prover9-apps, prover9-devel, prover9-doc), pvs-sbcl, sat4j, splint, stp (stp-devel), tex-zfuzz, why (why-coq, why-gwhy), zenon, csisat. | |||
Revision as of 15:10, 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.
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 aren't usually used directly by people; instead, they are a building block used by many other tools.
Packages:
- minisat2
- picosat
Other
The tools packaged so far, and not listed above, are: E, alt-ergo, coq (coq-coqide, coq-doc, coq-emacs), cvc3, emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO}, ppl (ppl-*), prover9 (prover9-apps, prover9-devel, prover9-doc), pvs-sbcl, sat4j, splint, stp (stp-devel), tex-zfuzz, why (why-coq, why-gwhy), zenon, csisat.