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
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)
A 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)
Other Support tools
There are various other lower-level routines that are necessary for some tools.
- ppl (ppl-*)