Formal Methods & Industry

Welcome to the Formal Methods Europe (FME) industry oriented website.

Events

Events related to formal methods.

Companies

Companies offering formal methods.

Users

Companies using formal methods.

Objectives

The objectives of the FME industrial committee and this website are as follows.

  1. Increase use of formal methods in industry.

  2. 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.

  3. 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.

  4. Increase collaboration between the formal methods community and industry.

Definition of Formal Methods

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.

Formal Methods

Below is a list of 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 Klaus Havelund havelund@gmail.com.

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.

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. 

Modeling

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.

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).

Companies Offering Formal Methods

This is a list of companies offering formal methods tools and/or consulting services.

  • AbsInt, France.

    • Tool: abstract interpretation (static analysis)
  • Clearsy, France.

    • Domain: railways
  • D-RisQ, UK.

    • The Kapture and ModelWorks frameworks use various formal methods.
    • The company has deep expertise in CSP and its model checker FDR4.
  • Verified Systems International GmbH, Bremen, Germany

    • Services: consulting, formal verification by model checking, abstract interpretation, or theorem proving, and conventional techniques are offered like review, code inspection, testing.
    • Tool: Model-based Testing Tool RT-Tester (RTT-MBT), based on formal SysML models, derives symbolic test cases as LTL formulas, creates concrete test data and procedures by SMT solving.
    • Tool: Source to Object Code Traceability Tool STO-Analyzer performs partial verification of object code against C-code, according to DAL-A verification requirements from RTCA DO-178C.
  • Verum

Companies using Formal Methods

This is a list of companies that use formal methods.

Company Tool
Airbus Astree static analyzer
Airbus Compcert verified compiler
Altran SPARK Ada toolset
Amazon Web Services TLA+
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
Facebook Infer static analyser
Microsoft SLAM
Rolls Royce Aeroengines SCADE
Rolls Royce Aeroengines SPARK Ada toolset

Applications of Formal Methods

This is a list of applications of formal methods in industry.

Events

  • FormaliSE 2021, International Conference on Formal Methods in Software Engineering, May 23-24, 2021, Madrid, Spain
  • Formal Methods 2021, Formal Methods conference, Nov 20-26, 2021, Beijing, China
  • I-Day@FM 2021, Industry Day of Formal Methods, One day during Nov 20-26, 2021, Beijing, China

Recent Posts

Meetings

December 2020 Meeting

December 2, 2020, FME Industry Committee meeting Present Jonathan Bowen Jan Friso Groote Colin O’Halloran John Hatcliff Klaus …

March 2020 Meeting

March 25, 2020, FME Industry Committee meeting Agenda To discuss which actions the industry committe should take on. Minutes The …

Papers

This is a list of various papers related to formal methods.

Title Authors Publication Year pdf
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 pdf
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 pdf

Members

The committee consists of the following members:

Chair of the committtee is Klaus Havelund.

List of previous members.