The FME Industry Committee maintains a list of tools to support formal methods.
You may submit your formal method by email to industry@fmeurope.org in case yours is not on the list.
Tools within each group are sorted alphabetically. A $-sign indicates that there is a commercial company behind and that acquisition of the tool is fee-based for industrial use.
PS: Note that the grouping of these tools is not ideal in several cases. A label system would be preferable and may be implemented in the near future.
Of General Interest
Websites offering surveys and categories of formal methods oriented tools.
Theorem Provers
A theorem prover usually supports a very expressive specification language (logic), such as e.g. classical higher order logic or constructive type theory, a proof system, and mechanized support for performing proofs. Proofs normally require manual effort, including providing loop invariants.
Rewrite Systems
Rewrite systems are based on so-called algebraic specification languages, where data types are specified by naming types (but not their contents), operations on those types, and equations between terms of operation applications. E.g. instead of specifying a stack as a list of elements, one specifies that pushing an element to a stack and then popping an element leaves us with the original stack. Rewrite systems perform rewriting of such terms. One may perceive rewrite systems as a sub-class of theorem provers.
Model Checkers
A model checker usually supports a specification language (logic) of limited expressiveness (compared to e.g. theorem proving langages), but where verification is fully automated. Focus is typically on specification and verification of concurrent systems.
SAT Solvers
SAT stands for Boolean SATisfiability (also called propositional satisfiability) and is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. SAT is fully automated.
SMT Solvers
SMT (Satisfiability Modulo Theories) is a generalization of the SAT problem, and is a form of the constraint satisfaction problem, which extends first-order logic with additional theories, such as e.g. real numbers, integers, and theories of various data structures such as lists, arrays, bit vectors and so on. Decision procedures decide satisfiablity of formulas in these extended logics. SMT is fully automated.
Static Analysis
Static program analysis is the analysis of computer software performed without actually executing programs. Analysis is performed on the source code or generated object code. Static analysis cannot verify functional correctness but focuses on detecting bad programming practices, and does so fully automatically and scalable.
Dynamic Analysis
Dynamic analysis is based on extracting information from a running system and using it to detect and possibly react to violation of certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications.
Model-based Testing
Model-based testing uses a formal model to test a System Under Test (SUT). The model can represent the desired behavior of the SUT, or can represent testing strategies and/or test environment.
- GraphWalker
- Reactis ($)
Modelling
Modelling is the activity of formalising a problem before it is solved, and/or it is the acticity modelling the solution at a high level of abstraction. As such this activity is common for all of the approaches mentioned on this page. However, this particular category is meant for approaches where the main focus is on modelling rather than on formal verification.
Synthesis
Synthesis involves generating code or a more detailed model from a high-level description. Such a description is typically in the form of sets of logical formulas or transition systems. The generated artefact is then guaranteed to meet the high-level description.
Verifiable Programming Languages
A verifiable programming language is a programming language supporting a logic for specifying functional correctness of code, e.g. pre/post conditions and invariants, and (usually) tool support for proving such properties of the code correct. Proofs normally require manual addition of lemmas (e.g. loop invariants).