From Fedora Project Wiki

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 methods tool suite ==
== 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.


Here are major categories of formal methods tools, along with the specific programs and packages that implement those categories in Fedora.
== Theorem Provers ==
They are organized in a way that (hopefully) makes them easier to understand.
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].
See the
[[FormalMethods|Fedora Formal Methods Special Interest Group (SIG)]]
for more information.


== Formal Specification Documentation Systems ==
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.
These tools let people express their specifications mathematically and check their types to eliminate simple errors.


* tex-zfuzz
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.


== Program Provers ==
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]).
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.


* frama-c {TODO}
=== Theorem Provers for First-Order Logic (FOL) ===
* splint
[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.
* why (why-coq, why-gwhy).


== Program Model Checkers ==
Supported Upstream Projects (names of available packages):
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.
* [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)


* BLAST {todo}
=== 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.


== Model Checkers ==
Supported Upstream Projects (names of available packages):
Model checkers can take abstract specifications, turn them into a "model" of state transitions, and then determine if this model will meet certain requirements.
* [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)


* divine-mc {todo}
=== GUI Proof Assistants ===
These systems help people use interactive provers by providing a graphical interface to them.


== Theorem Provers ==
Supported Upstream Projects (names of available packages):
Theorem provers can prove whether or not a goal can be proved given a set of assumptionsThese goals and assumptions are stated in some mathematical languageTheorem provers can be categorized by the kind of mathematical language it accepts.
* [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 quicklyMost 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).


=== First-Order Logic (FOL) Theorem Provers ===
Depending on the application domain of interest, an SMT problem includes a "base" theory that must also be satisfied by the solutionThis 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.
[http://en.wikipedia.org/wiki/First-order_logic First-order Logic (FOL)] is a widely-used mathematical language for stating assumptions and goalsFOL 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
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)]. 
* prover9 (prover9-apps, prover9-devel, prover9-doc)


=== Higher-Order Logic (HOL) Theorem Provers ===
Supported Upstream Projects (names of available packages):
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.
* [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)


* coq (coq-coqide, coq-doc, coq-emacs)
== Formal Specification Languages ==
* PVS (pvs-sbcl)
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.


=== Helper systems for interactive provers ===
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 systems help people use interactive provers.


* Proof General
Supported Upstream Projects (names of available packages):
** emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch)
* [http://spivey.oriel.ox.ac.uk/mike/fuzz/ Type Checker and LaTeX Style for Z] (tex-zfuzz)
** xemacs-proofgeneral (xemacs-proofgeneral-el),


== Satisfiability Modulo Theories (SMT) Solvers ==
== Tools for Validation, Verification ==
[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).
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 addition, SMT Solvers support one or more "theories", i.e., a set of predefined functions/predicates.
For example, it may include a "theory" for numbers that defines
adding, multiplying, and comparing numbers.
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
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.
* alt-ergo
* stp (stp-devel)
* zenon
* csisat


FIXME: csisat is really an interpolator that can be used to SMT-like solving; should it go into a different category?
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.


== SAT Solvers ==
Supported Upstream Projects (names of available packages):
A [http://en.wikipedia.org/wiki/Boolean_satisfiability_problem SAT (satisfiability) solver] can determine if boolean variables
* [http://flocq.gforge.inria.fr/ Floats for Coq] (flocq, flocq-source)
(variables which can be true or false) can have values that
* [http://frama-c.com/ Framework for Modular Analysis of C programs] (frama-c)
would make a set of formulas true.
* [http://gappa.gforge.inria.fr/ Génération Automatique de Preuves de Propriétés Arithmétiques] (gappa, gappalib-coq)
If it's possible, then the formulas are ''satisfiable''.
* [http://why.lri.fr/ Why 2] (why, why-all, why-coq, why-gwhy, why-jessie, why-pvs-support)
In the worst case this problem is extremely hard
* [http://why3.lri.fr/ Why 3] (why3, why3-emacs)
(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 are often used as a building block to develop other tools.


Packages:
== Other Tools ==
* minisat2
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.
* picosat
* sat4j


== Other Support tools ==
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.
There are various other lower-level routines that are necessary for some tools.


* 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):

  • E (E)
  • Prover9 (prover9, prover9-apps, prover9-devel, prover9-doc)
  • Zenon (zenon)

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):

  • Coq (coq, coq-doc, coq-emacs-el, coq-emacs, coq-xemacs-el, coq-xemacs)
  • 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):

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):

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):

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):

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):