Welcome to the Formal Methods Europe (FME) industry oriented website.
Events related to formal methods.
Companies offering formal methods.
Companies using formal methods.
The objectives of the FME industrial committee and this website are as follows.
Increase use of formal methods in industry.
Increase awareness in industry of formal methods. This includes informing the industry about which formal methods are available, which companies use formal methods, which companies offer formal methods and consultancy, industrial success stories of formal methods, and other relevant material such as links to papers concerned with the above aspects. It also includes announcement of industrially oriented events.
Increase awareness in the formal methods community of industrial use of formal methods. This forms a feedback on what works and what does not work in practice, and can help steer the formal methods community towards successful approaches.
Increase collaboration between the formal methods community and industry.
It can be difficult to precisely define what is a formal method. A popular formulation is that it is a technique for developing correct software which is based on mathematical rigorius principles. The Wikipedia offers a more elaborate definition.
The benefit of using formal methods is intended to be more reliable software and hardware systems. Also productivity gains can be expected with some methods. Some formal methods provide a structured rigorous way to think about a problem up front, which in itself has advantages (even in lack of tool support). Other formal methods are code oriented, and can ensure that written code is correct.
This video contains an interview with three industial engineers on the topic: Formal Methods in the Industrial Domain.
Below is a list of tools to support formal methods.
Submit your formal method here in case it is not on the list. You may also submit comments to the website. Or: simply send an email to Tim Willemse T.A.C.Willemse@TUe.nl.
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.
Websites offering surveys and categories of formal methods oriented tools.
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 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.
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 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 (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 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 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 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.
Modeling is the activity of formalizing a problem before it is solved, and/or it is the acticity modeling 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 modeling rather than on formal verification.
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).
This is a list of companies offering formal methods tools and/or consulting services.
AbsInt, France.
Clearsy, France.
D-RisQ, UK.
Verified Systems International GmbH, Bremen, Germany
This is a list of companies that use formal methods.
| Company | Tool |
|---|---|
| Airbus | Astree static analyzer |
| Airbus | Compcert verified compiler |
| Altran | SPARK Ada toolset |
| AWS | Dafny |
| AWS | TLA+ |
| AWS | Z3 |
| Atkins | MALPAS Software Static Analysis Toolset |
| BAES | SPARK Ada toolset |
| ClearSy | Atelier B (for railway control) |
| Callen Lenz | Kapture |
| Callen Lenz | ModelWorks |
| D-RisQ | FDR4 |
| D-RisQ | Z3 |
| D-RisQ | ProofPower |
| D-RisQ | Temporal logic predicates used to check consistency within Kapture for software requirements |
| D-RisQ | ModelWorks for verification of Simulink/Stateflow designs against high level software requirements |
| D-RisQ | CLawZ for verification of C code automatically generated from Simulink/Stateflow Used on various Robotics and Autonomous Systems |
| Galois | Software Analysis Workbench (used to verify Amazon Web Services s2n encryption library) |
| Honeywell | PVS |
| Honeywell | Kapture |
| Honeywell | Variety of SMT solvers |
| Infer static analyser | |
| Microsoft | SLAM |
| NASA | PVS |
| NASA | Spin |
| Rolls Royce Aeroengines | SCADE |
| Rolls Royce Aeroengines | SPARK Ada toolset |
This is a list of applications of formal methods in industry.
This is a list of various papers related to formal methods.
| Title | Authors | Publication | Year | |
|---|---|---|---|---|
| Formal Methods in Dependable Systems Engineering: a Survey of Professionals from Europe and North America | Mario Gleirscher and Diego Marmsoler | Empirical Software Engineering https://link.springer.com/article/10.1007/s10664-020-09836-5. Archived version including quotes: https://arxiv.org/abs/1812.08815 | 2020 | |
| The 2020 Expert Survey on Formal Methods | Hubert Garavel, Maurice H. ter Beek, and Jaco van de Pol | FMICS 2020, LNCS 12327 https://doi.org/10.1007/978-3-030-58298-2_1 | 2020 |
The committee consists of the following members:
