Companies Offering Formal Methods

The FME Industry Committee maintains a list of companies offering formal methods tools and/or consulting services. If your company is not on this list but you would like to have it appear on there, then send an email to industry@fmeurope.org.

  • AbsInt, France.

    • Tool: abstract interpretation (static analysis)

  • AtkinsRéalis, Canada.

    • Tool: MALPAS, a static analysis tool used in various domains, including Nuclear, Aerospace, and Defence.

  • 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

Share