(A face lift for the SMT Solver section. Reordered the SAT and SMT sections to make it easier to explain what they are.) |
|||
| Line 1: | Line 1: | ||
== Formal | == 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. | Here are major categories of formal methods tools, along with the specific programs and packages that implement those categories in Fedora. | ||
They are organized in a way that (hopefully) makes them easier to understand. | They are organized in a way that (hopefully) makes them easier to understand. | ||
See the | See the [[FormalMethods|Fedora Formal Methods Special Interest Group (SIG)]] | ||
[[FormalMethods|Fedora Formal Methods Special Interest Group (SIG)]] | |||
for more information. | for more information. | ||
== Formal Specification | == Formal Specification Systems == | ||
These tools let people express their specifications mathematically and check their types to eliminate simple errors. | These tools let people express their specifications mathematically and check their types to eliminate simple errors. | ||
Supported Upstream Projects (names of available packages): | |||
* tex-zfuzz | * tex-zfuzz | ||
| Line 15: | Line 15: | ||
These tools accept input in a programming language, as well as annotations about its requirements (e.g., as preconditions and postconditions), and prove that the program meets its requirements. | These tools accept input in a programming language, as well as annotations about its requirements (e.g., as preconditions and postconditions), and prove that the program meets its requirements. | ||
Supported Upstream Projects (names of available packages): | |||
* frama-c {TODO} | * frama-c {TODO} | ||
* splint | * splint | ||
| Line 22: | Line 23: | ||
Program model checkers can take programs written in a programming language, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements. | Program model checkers can take programs written in a programming language, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements. | ||
Supported Upstream Projects (names of available packages): | |||
* BLAST {todo} | * BLAST {todo} | ||
| Line 27: | Line 29: | ||
Model checkers can take abstract specifications, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements. | Model checkers can take abstract specifications, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements. | ||
Supported Upstream Projects (names of available packages): | |||
* divine-mc {todo} | * divine-mc {todo} | ||
| Line 35: | Line 38: | ||
[http://en.wikipedia.org/wiki/First-order_logic 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). | [http://en.wikipedia.org/wiki/First-order_logic 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 | Supported Upstream Projects (names of available packages): | ||
* prover9 (prover9-apps, prover9-devel, prover9-doc) | * [http://www.eprover.org/ E] (E) | ||
* [http://www.cs.unm.edu/~mccune/prover9/ Prover9] (prover9, prover9-apps, prover9-devel, prover9-doc) | |||
* [http://focal.inria.fr/zenon/ Zenon] (zenon) | |||
=== Higher-Order Logic (HOL) Theorem Provers === | === Higher-Order Logic (HOL) Theorem Provers === | ||
Higher-order Logics (HOLs) are a family of mathematical languages for stating assumptions and goals. They remove many of the limitations of FOL, making them more expressive, but this makes it more difficult for tools to automatically find proofs. Thus, HOL systems tend to work interactively; humans guide the tool towards a proof. | Higher-order Logics (HOLs) are a family of mathematical languages for stating assumptions and goals. They remove many of the limitations of FOL, making them more expressive, but this makes it more difficult for tools to automatically find proofs. Thus, HOL systems tend to work interactively; humans guide the tool towards a proof. | ||
* coq (coq- | Supported Upstream Projects (names of available packages): | ||
* PVS (pvs-sbcl) | * [http://coq.inria.fr/ Coq] (coq, coq-doc, coq-emacs-el, coq-emacs, coq-xemacs-el, coq-xemacs) | ||
* [http://pvs.csl.sri.com/ PVS] (pvs-sbcl) | |||
=== | === GUI Proof Assistants === | ||
These systems help people use interactive provers. | These systems help people use interactive provers. | ||
Supported Upstream Projects (names of available packages): | |||
* [http://coq.inria.fr/ CoqIDE] (coq-coqide) | |||
* | * [http://proofgeneral.inf.ed.ac.uk/ Proof General for Emacs] (emacs-common-proofgeneral, emacs-proofgeneral, emacs-proofgeneral-el) | ||
* [http://proofgeneral.inf.ed.ac.uk/ Proof General for XEmacs] (xemacs-proofgeneral, xemacs-proofgeneral-el) | |||
[http:// | |||
== Boolean Satisfiability (SAT) Solvers == | == Boolean Satisfiability (SAT) Solvers == | ||
| Line 74: | Line 63: | ||
In the worst case, the Boolean Satisfiability problem can be difficult enough to be impractical to solve. (The first algorithm proven to be [http://en.wikipedia.org/wiki/NP-complete NP-complete] was the Boolean Satisfiability problem). However, most contemporary SAT Solvers can solve a wide class of interesting and practical problems surprisingly quickly. Most SAT Solvers are based on some variant of the [http://en.wikipedia.org/wiki/DPLL_algorithm Davis-Putnam-Logemann-Loveland (DPLL) algorithm]. The performance of SAT Solvers can also be attributed to the use of very efficient data structures in their implementations. | In the worst case, the Boolean Satisfiability problem can be difficult enough to be impractical to solve. (The first algorithm proven to be [http://en.wikipedia.org/wiki/NP-complete NP-complete] was the Boolean Satisfiability problem). However, most contemporary SAT Solvers can solve a wide class of interesting and practical problems surprisingly quickly. Most SAT Solvers are based on some variant of the [http://en.wikipedia.org/wiki/DPLL_algorithm Davis-Putnam-Logemann-Loveland (DPLL) algorithm]. The performance of SAT Solvers can also be attributed to the use of very efficient data structures in their implementations. | ||
For a given class of problems (e.g. Satisfiable vs. Unsatisfiable), the performance of SAT Solvers can vary quite a bit. Fortunately, the almost universal adoption of the DIMACS [http://en.wikipedia.org/wiki/Conjunctive_normal_form conjunctive normal form | For a given class of problems (e.g. Satisfiable vs. Unsatisfiable), the performance of SAT Solvers can vary quite a bit. Fortunately, the almost universal adoption of the DIMACS [http://en.wikipedia.org/wiki/Conjunctive_normal_form conjunctive normal form (CNF)] input format by the community makes the task of comparing the performance of SAT Solvers relatively easy. SAT solvers are often used as building blocks for the construction of more sophisticated tools, (such as "eager" [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories SMT] Solvers). | ||
Supported Upstream Projects (names of available packages): | Supported Upstream Projects (names of available packages): | ||
| Line 82: | Line 71: | ||
* [http://fmv.jku.at/picosat/ picoSAT] (picosat) | * [http://fmv.jku.at/picosat/ picoSAT] (picosat) | ||
* [http://www.sat4j.org/ Sat4j] (sat4j) | * [http://www.sat4j.org/ Sat4j] (sat4j) | ||
== Satisfiability Modulo Theories (SMT) Solvers == | |||
The [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisfiability Modulo Theories (SMT)] problem is a generalization of the Boolean Satisfiability problem where the set of formulas to be satisfied are from the (more expressive) language of [http://en.wikipedia.org/wiki/First-order_logic First-Order Logic (FOL)]. Formulas can contain predicates and functions whose arguments are (usually, but not always, unquantified) variables that correspond to objects from a "universe" that will depend on the application at hand, (e.g. bit vectors, real numbers). A solution to a given SMT problem must include a specific interpretation of these variables (this is the the notion of semantic truth introduced by [http://en.wikipedia.org/wiki/Alfred_Tarski Tarski] in 1933). | |||
Depending on the application domain of interest, an SMT problem includes a "base" theory that must also be satisfied by the solution. This might be the theory of bit vectors for hardware design applications, the theory of arrays and lists for software verification applications, or rational arithmetic for mathematical or scientific applications. | |||
The SMT Solver community has collaborated to develop a standardized set of base theories, and input and output languages for SMT Solvers, collectively known as the [http://www.smt-lib.org/ Satisfiability Modulo Theories Library (SMT-LIB)]. | |||
Supported Upstream Projects (names of available packages): | |||
* [http://alt-ergo.lri.fr/ Alt-Ergo] (alt-ergo, alt-ergo-gui) | |||
* [http://csisat.googlecode.com/ CSIsat] (csisat) | |||
* [http://www.cs.nyu.edu/acsys/cvc3/ CVC3] (cvc3, cvc3-devel, cvc3-doc, cvc3-emacs, cvc3-emacs-el, cvc3-java, cvc3-xemacs, cvc3-xemacs-el) | |||
* [http://www.cs.unm.edu/~mccune/prover9/ Mace4] (prover9) | |||
* [http://sourceforge.net/projects/stp-fast-prover/ STP] (stp, stp-devel) | |||
== Other Support tools == | == Other Support tools == | ||
Revision as of 06:19, 18 October 2012
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. They are organized in a way that (hopefully) makes them easier to understand. See the Fedora Formal Methods Special Interest Group (SIG) for more information.
Formal Specification Systems
These tools let people express their specifications mathematically and check their types to eliminate simple errors.
Supported Upstream Projects (names of available packages):
- tex-zfuzz
Program Provers
These tools accept input in a programming language, as well as annotations about its requirements (e.g., as preconditions and postconditions), and prove that the program meets its requirements.
Supported Upstream Projects (names of available packages):
- frama-c {TODO}
- splint
- why (why-coq, why-gwhy).
Program Model Checkers
Program model checkers can take programs written in a programming language, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements.
Supported Upstream Projects (names of available packages):
- BLAST {todo}
Model Checkers
Model checkers can take abstract specifications, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements.
Supported Upstream Projects (names of available packages):
- divine-mc {todo}
Theorem Provers
Theorem provers can prove whether or not a goal can be proved given a set of assumptions. These goals and assumptions are stated in some mathematical language. Theorem provers can be categorized by the kind of mathematical language it accepts.
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).
Supported Upstream Projects (names of available packages):
Higher-Order Logic (HOL) Theorem Provers
Higher-order Logics (HOLs) are a family of mathematical languages for stating assumptions and goals. They remove many of the limitations of FOL, making them more expressive, but this makes it more difficult for tools to automatically find proofs. Thus, HOL systems tend to work interactively; humans guide the tool towards a proof.
Supported Upstream Projects (names of available packages):
GUI Proof Assistants
These systems help people use interactive provers.
Supported Upstream Projects (names of available packages):
- CoqIDE (coq-coqide)
- Proof General for Emacs (emacs-common-proofgeneral, emacs-proofgeneral, emacs-proofgeneral-el)
- Proof General for XEmacs (xemacs-proofgeneral, xemacs-proofgeneral-el)
Boolean Satisfiability (SAT) Solvers
Given a set of well formed formulas from Boolean or Propositional Logic, a Boolean Satisfiability (SAT) solver attempts to determine if there is an assignment of values (true or false) to the boolean variables that appear in the formulas, such that every formula evaluates to true. If one or more such solutions exist, the set of formulas is said to be Satisfiable. If no such solutions exist, the set of formulas is said to be Unsatisfiable.
In the worst case, the Boolean Satisfiability problem can be difficult enough to be impractical to solve. (The first algorithm proven to be NP-complete was the Boolean Satisfiability problem). However, most contemporary SAT Solvers can solve a wide class of interesting and practical problems surprisingly quickly. Most SAT Solvers are based on some variant of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. The performance of SAT Solvers can also be attributed to the use of very efficient data structures in their implementations.
For a given class of problems (e.g. Satisfiable vs. Unsatisfiable), the performance of SAT Solvers can vary quite a bit. Fortunately, the almost universal adoption of the DIMACS conjunctive normal form (CNF) input format by the community makes the task of comparing the performance of SAT Solvers relatively easy. SAT solvers are often used as building blocks for the construction of more sophisticated tools, (such as "eager" SMT Solvers).
Supported Upstream Projects (names of available packages):
- CryptoMiniSat (cryptominisat, cryptominisat-libs, cryptominisat-devel)
- GlueMiniSat (glueminisat)
- MiniSat 2 (minisat2)
- picoSAT (picosat)
- Sat4j (sat4j)
Satisfiability Modulo Theories (SMT) Solvers
The Satisfiability Modulo Theories (SMT) problem is a generalization of the Boolean Satisfiability problem where the set of formulas to be satisfied are from the (more expressive) language of First-Order Logic (FOL). Formulas can contain predicates and functions whose arguments are (usually, but not always, unquantified) variables that correspond to objects from a "universe" that will depend on the application at hand, (e.g. bit vectors, real numbers). A solution to a given SMT problem must include a specific interpretation of these variables (this is the the notion of semantic truth introduced by Tarski in 1933).
Depending on the application domain of interest, an SMT problem includes a "base" theory that must also be satisfied by the solution. This might be the theory of bit vectors for hardware design applications, the theory of arrays and lists for software verification applications, or rational arithmetic for mathematical or scientific applications.
The SMT Solver community has collaborated to develop a standardized set of base theories, and input and output languages for SMT Solvers, collectively known as the Satisfiability Modulo Theories Library (SMT-LIB).
Supported Upstream Projects (names of available packages):
- Alt-Ergo (alt-ergo, alt-ergo-gui)
- CSIsat (csisat)
- CVC3 (cvc3, cvc3-devel, cvc3-doc, cvc3-emacs, cvc3-emacs-el, cvc3-java, cvc3-xemacs, cvc3-xemacs-el)
- Mace4 (prover9)
- STP (stp, stp-devel)
Other Support tools
There are various other lower-level routines that are necessary for some tools.
- ppl (ppl-*)