m (Added some additional formal specification languages that might be candidates for future addition to Fedora (though many of them seem to have licensing issues that would preculde that from happening).) |
|||
| (8 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
== Formal | == Formal Methods Tool Suite == | ||
This page presents the suite of open source licensed formal methods tools that are currently packaged in Fedora. They have been organized in a way that (hopefully) makes what they can do and how they do it easier to understand. For more information about formal methods, and open source licensed formal methods tools that are not (yet) packaged in Fedora, see the [[FormalMethods|Fedora Formal Methods Special Interest Group (SIG)]] page for more information. | |||
== Theorem Provers == | |||
The question of what constitutes an acceptable proof of a given conjecture has been a controversial and heated topic in the field of Mathematics that goes back many centuries. One solution to this controversy was the development of what is called a [http://en.wikipedia.org/wiki/Formal_proof Formal Proof]. | |||
[ | |||
In a formal proof, the assumptions or axioms and the conjecture to be proven must first be expressed in a [http://en.wikipedia.org/wiki/Formal_language Formal Language], which differs in many significant ways from the written or spoken languages that we are accustomed to in our daily activities. The most significant difference is that the process of determining if a given statement or formula is well formed (that it adheres to all the rules of the formal language) is mechanical and unambiguous. | |||
A formal proof starts with a set of formulas that represent the assumptions or axioms. A sequence of new formulas or intermediate theorems are generated by applying an accepted inference rule, such as [http://en.wikipedia.org/wiki/Modus_ponens Modus Ponens]. A formal proof is then just a finite sequence of such formulas, where the last formula in the sequence corresponds to the conjecture to be proven. One of the motivations for the development of formal proofs was so that a human without extensive Mathematical training or even a machine could be employed to unambiguously check the validity of a proof, or even to find new proofs. | |||
Theorem Provers are programs that attempt to generate formal proofs of a given conjecture. They may do so with the assistance of a human operator (Guided or Interactive Theorem Provers) or work totally on their own ([http://en.wikipedia.org/wiki/Automated_theorem_proving Automated Theorem Provers]). | |||
=== Theorem Provers for First-Order Logic (FOL) === | |||
[http://en.wikipedia.org/wiki/First-order_logic First-order Logic (FOL), or Predicate Logic] is one of the most widely used formal languages. Many theorem provers for FOL can find proofs automatically, without any user intervention. Theorem provers for FOL often, though not always, employ an inference rule called [http://en.wikipedia.org/wiki/Resolution_%28logic%29 resolution]. The more intuitive [http://en.wikipedia.org/wiki/Modus_ponens Modus Ponens] inference rule is a special case of resolution. | |||
Supported Upstream Projects (names of available packages): | |||
* [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) | |||
=== Theorem Provers for Higher-Order Logic (HOL) === | |||
[http://en.wikipedia.org/wiki/Higher-order_logic Higher-order Logic (HOL)] is an extension to FOL which facilitates the expression of more complex concepts. The most common extension is to allow quantifiers to refer to predicates, but there are many other variations. The greater expressive power of HOL comes with a price, as formal proofs are more difficult to construct. Most theorem provers for HOL are guided or interactive in nature. | |||
Supported Upstream Projects (names of available packages): | |||
* [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 by providing a graphical interface to them. | |||
== | 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) | |||
== Boolean Satisfiability (SAT) Solvers == | |||
Given a set of well formed formulas from [http://en.wikipedia.org/wiki/Propositional_calculus Boolean or Propositional Logic], a [http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 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 problem 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 (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): | |||
* [http://www.msoos.org/cryptominisat2 CryptoMiniSat] (cryptominisat, cryptominisat-libs, cryptominisat-devel) | |||
* [http://glueminisat.nabelab.org/ GlueMiniSat] (glueminisat) | |||
* [http://minisat.se/ MiniSat 2] (minisat2) | |||
* [http://fmv.jku.at/picosat/ picoSAT] (picosat) | |||
* [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) | |||
== Formal Specification Languages == | |||
In mission critical applications (where a mistake might cause great financial loss, or even loss of life), hardware and/or software designs are often formulated at an abstracted level using some type of [http://en.wikipedia.org/wiki/Specification_language Formal Specification Language]. Formal methods can then be applied to the specification to prove or refute theorems related to both validation and verification issues. | |||
There are a growing number of formal specification languages for which useful open source licensed, or no cost licensed development tools are available. These include, but are not limited to; [http://en.wikipedia.org/wiki/Alloy_(specification_language) Alloy], [http://en.wikipedia.org/wiki/B-Method B-Method Specification Language and Event-B], [http://en.wikipedia.org/wiki/VDM_Specification_Language Vienna Development Method Specification Language (VDM-SL)] and [http://en.wikipedia.org/wiki/Z_notation Z Notation] languages. | |||
These | |||
Supported Upstream Projects (names of available packages): | |||
* [http://spivey.oriel.ox.ac.uk/mike/fuzz/ Type Checker and LaTeX Style for Z] (tex-zfuzz) | |||
* | |||
== | == Tools for Validation, Verification == | ||
[http://en.wikipedia.org/wiki/ | The discovery of the [http://en.wikipedia.org/wiki/FDIV_Bug FDIV Bug] in Intel's Pentium processor in 1994 was a huge catalyst for the development of new formal specification languages and related formal methods tools for the design of microprocessors. Many languages and tools have been developed since then, but most of them are commercial products. However, many of the open source SMT Solvers listed above can be readily used as building blocks for hardware validation and verification applications. | ||
In the area of software development, there are a growing number of open source licensed formal methods tools. The most sophisticated tools are designed to work with specifications written in specialized formal specification languages. Embedding specifications (in the form of specially crafted comments) directly in an existing program written in a procedural programming language such as C, or Java is another approach that is gaining popularity. There is also a growing class of "lightweight" formal methods tools that work directly on an existing, unmodified (or slightly modified) program written in a procedural programming language. Naturally, the scope of what the later systems can accomplish is more limited. | |||
It should be noted that it is not possible to validate or verify a software design or program in a manner that entirely precludes something bad from happening. Validation and/or verification can only be only be accomplished relative to the agreed upon specification. The most common way that formal methods tools are used is to prove conjectures that the design or software implementation has some specific, and desired property (e.g. that a program never becomes "deadlocked"). Another valuable category of formal methods tools are those designed to find a counter-example to a desirable conjecture. This is more colloquially known as finding a "bug" or flaw. | |||
Supported Upstream Projects (names of available packages): | |||
* [http://flocq.gforge.inria.fr/ Floats for Coq] (flocq, flocq-source) | |||
( | * [http://frama-c.com/ Framework for Modular Analysis of C programs] (frama-c) | ||
* [http://gappa.gforge.inria.fr/ Génération Automatique de Preuves de Propriétés Arithmétiques] (gappa, gappalib-coq) | |||
* [http://why.lri.fr/ Why 2] (why, why-all, why-coq, why-gwhy, why-jessie, why-pvs-support) | |||
* [http://why3.lri.fr/ Why 3] (why3, why3-emacs) | |||
( | |||
== Other Tools == | |||
These tools did not fit into any one of the categories above, but are related to computational logic or formal methods. Also included are any prerequisites for a package listed above. | |||
For the sake of providing an example of a software project developed with the help of formal methods tools, the [http://lipforge.ens-lyon.fr/www/crlibm/ Correctly Rounded mathematical library] is included in the list below. | |||
* ppl (ppl- | Supported Upstream Projects (names of available packages): | ||
* [http://perso.b2b2c.ca/sarrazip/dev/boolstuff.html BoolStuff] (boolstuff, booldnf) | |||
* [http://vlsi.colorado.edu/~fabio/CUDD/ CU Decision Diagrams] (cudd) | |||
* [http://lipforge.ens-lyon.fr/www/crlibm/ Correctly Rounded mathematical library] (crlibm) | |||
* [http://www.cs.unipr.it/ppl/ Parma Polyhedra Library] (ppl, ppl-devel, ppl-docs, ppl-gprolog, ppl-gprolog-static, ppl-java, ppl-java-javadoc, ppl-pwl, ppl-pwl-devel, ppl-pwl-docs, ppl-pwl-static, ppl-static, ppl-swiprolog, ppl-swiprolog-static, ppl-utils, ppl-yap) | |||
Latest revision as of 23:52, 28 January 2013
Formal Methods Tool Suite
This page presents the suite of open source licensed formal methods tools that are currently packaged in Fedora. They have been organized in a way that (hopefully) makes what they can do and how they do it easier to understand. For more information about formal methods, and open source licensed formal methods tools that are not (yet) packaged in Fedora, see the Fedora Formal Methods Special Interest Group (SIG) page for more information.
Theorem Provers
The question of what constitutes an acceptable proof of a given conjecture has been a controversial and heated topic in the field of Mathematics that goes back many centuries. One solution to this controversy was the development of what is called a Formal Proof.
In a formal proof, the assumptions or axioms and the conjecture to be proven must first be expressed in a Formal Language, which differs in many significant ways from the written or spoken languages that we are accustomed to in our daily activities. The most significant difference is that the process of determining if a given statement or formula is well formed (that it adheres to all the rules of the formal language) is mechanical and unambiguous.
A formal proof starts with a set of formulas that represent the assumptions or axioms. A sequence of new formulas or intermediate theorems are generated by applying an accepted inference rule, such as Modus Ponens. A formal proof is then just a finite sequence of such formulas, where the last formula in the sequence corresponds to the conjecture to be proven. One of the motivations for the development of formal proofs was so that a human without extensive Mathematical training or even a machine could be employed to unambiguously check the validity of a proof, or even to find new proofs.
Theorem Provers are programs that attempt to generate formal proofs of a given conjecture. They may do so with the assistance of a human operator (Guided or Interactive Theorem Provers) or work totally on their own (Automated Theorem Provers).
Theorem Provers for First-Order Logic (FOL)
First-order Logic (FOL), or Predicate Logic is one of the most widely used formal languages. Many theorem provers for FOL can find proofs automatically, without any user intervention. Theorem provers for FOL often, though not always, employ an inference rule called resolution. The more intuitive Modus Ponens inference rule is a special case of resolution.
Supported Upstream Projects (names of available packages):
Theorem Provers for Higher-Order Logic (HOL)
Higher-order Logic (HOL) is an extension to FOL which facilitates the expression of more complex concepts. The most common extension is to allow quantifiers to refer to predicates, but there are many other variations. The greater expressive power of HOL comes with a price, as formal proofs are more difficult to construct. Most theorem provers for HOL are guided or interactive in nature.
Supported Upstream Projects (names of available packages):
GUI Proof Assistants
These systems help people use interactive provers by providing a graphical interface to them.
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 problem 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)
Formal Specification Languages
In mission critical applications (where a mistake might cause great financial loss, or even loss of life), hardware and/or software designs are often formulated at an abstracted level using some type of Formal Specification Language. Formal methods can then be applied to the specification to prove or refute theorems related to both validation and verification issues.
There are a growing number of formal specification languages for which useful open source licensed, or no cost licensed development tools are available. These include, but are not limited to; Alloy, B-Method Specification Language and Event-B, Vienna Development Method Specification Language (VDM-SL) and Z Notation languages.
Supported Upstream Projects (names of available packages):
- Type Checker and LaTeX Style for Z (tex-zfuzz)
Tools for Validation, Verification
The discovery of the FDIV Bug in Intel's Pentium processor in 1994 was a huge catalyst for the development of new formal specification languages and related formal methods tools for the design of microprocessors. Many languages and tools have been developed since then, but most of them are commercial products. However, many of the open source SMT Solvers listed above can be readily used as building blocks for hardware validation and verification applications.
In the area of software development, there are a growing number of open source licensed formal methods tools. The most sophisticated tools are designed to work with specifications written in specialized formal specification languages. Embedding specifications (in the form of specially crafted comments) directly in an existing program written in a procedural programming language such as C, or Java is another approach that is gaining popularity. There is also a growing class of "lightweight" formal methods tools that work directly on an existing, unmodified (or slightly modified) program written in a procedural programming language. Naturally, the scope of what the later systems can accomplish is more limited.
It should be noted that it is not possible to validate or verify a software design or program in a manner that entirely precludes something bad from happening. Validation and/or verification can only be only be accomplished relative to the agreed upon specification. The most common way that formal methods tools are used is to prove conjectures that the design or software implementation has some specific, and desired property (e.g. that a program never becomes "deadlocked"). Another valuable category of formal methods tools are those designed to find a counter-example to a desirable conjecture. This is more colloquially known as finding a "bug" or flaw.
Supported Upstream Projects (names of available packages):
- Floats for Coq (flocq, flocq-source)
- Framework for Modular Analysis of C programs (frama-c)
- Génération Automatique de Preuves de Propriétés Arithmétiques (gappa, gappalib-coq)
- Why 2 (why, why-all, why-coq, why-gwhy, why-jessie, why-pvs-support)
- Why 3 (why3, why3-emacs)
Other Tools
These tools did not fit into any one of the categories above, but are related to computational logic or formal methods. Also included are any prerequisites for a package listed above.
For the sake of providing an example of a software project developed with the help of formal methods tools, the Correctly Rounded mathematical library is included in the list below.
Supported Upstream Projects (names of available packages):
- BoolStuff (boolstuff, booldnf)
- CU Decision Diagrams (cudd)
- Correctly Rounded mathematical library (crlibm)
- Parma Polyhedra Library (ppl, ppl-devel, ppl-docs, ppl-gprolog, ppl-gprolog-static, ppl-java, ppl-java-javadoc, ppl-pwl, ppl-pwl-devel, ppl-pwl-docs, ppl-pwl-static, ppl-static, ppl-swiprolog, ppl-swiprolog-static, ppl-utils, ppl-yap)