Formal methods tool suite

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?

SAT Solvers

A SAT (satisfiability) solver can determine if boolean variables (variables which can be true or false) can have values that would make a set of formulas true. If it's possible, then the formulas are satisfiable. In the worst case this problem is extremely hard (i.e., they are NP-complete), but modern algorithms can usually solve typical SAT problems very quickly. SAT Solvers often accept the "DIMACS conjunctive normal form (CNF)" input format. SAT solvers are often used as a building block to develop other tools.

Packages:

• minisat2
• picosat
• sat4j

Other Support tools

There are various other lower-level routines that are necessary for some tools.

• ppl (ppl-*)