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 Documentation Systems
These tools let people express their specifications mathematically and check their types to eliminate simple errors.
- 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.
- 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.
- 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.
- 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).
- E
- prover9 (prover9-apps, prover9-devel, prover9-doc)
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.
- coq (coq-coqide, coq-doc, coq-emacs)
- PVS (pvs-sbcl)
Helper systems for interactive provers
These systems help people use interactive provers.
- Proof General
- emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch)
- xemacs-proofgeneral (xemacs-proofgeneral-el),
Satisfiability Modulo Theories (SMT) Solvers
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). 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. Variables can have values other than true or false (e.g., they may be numbers). Many of these tools support the SMT-LIB input format. SAT solvers are often used as a building block to develop other tools.
- cvc3
- 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?
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)
Other Support tools
There are various other lower-level routines that are necessary for some tools.
- ppl (ppl-*)