About Us Products Articles News Contact Support

Formal Methods Toolkit

Formal Methods Toolkit is a set of extension packages for Mathematica, supporting software engineering activities related to modeling, verification and code generation of correct software systems. Even though not limited to any particular domain, FMT was motivated by the needs of embedded and safety-critical projects.

The major features of FMT are:

• understandable level of abstraction
• operation pre-conditions, post-conditions and type invariants
• loop invariants and variants
• ghost variables
• visualization and analysis tools for architecture, call graphs, control flow and data relations
• advanced modeling techniques - metaprogramming and code synthesis
• code generators for Ada, MISRA-C and MISRA-C++
• seamless integration with Mathematica, enabling ultimate extensibility and automation

Formal Methods Toolkit relies on Mathematica as its underlying computing platform and is portable between Linux, Mac OS X and Windows. Both content-rich, interactive workflows with notebook files and batch processing with Wolfram scripting are supported.

Prior experience with Wolfram and Mathematica is not necessary to use and benefit from FMT, although some knowledge of that platform can bring significant added value with advanced modeling techniques and automation capabilities.

Example gallery

Check the gallery of example screenshots to see how FMT can help you create better software:

Documentation

"Formal Methods Toolkit" by Maciej Sobczak This book is a complete FMT manual that describes its features and usage patterns. The on-line version of this book is available as well.

Apart from this comprehensive manual, a set of example notebooks for interactive exploration is included as part of the downloadable package below.

Video materials

The YouTube playlist presenting the idea to use Mathematica for formal methods. These videos explain not only how to use FMT, but also what features of Mathematica and Wolfram were used as a basis for its implementation.

Development blog

The articles linked below document the reasoning behind new FMT features. All features listed below are part of the FMT 2.0 release.

Implementing Logic Reachability Checks

Basic Support For Ghost Variables

Supporting Quantified Statements, Part 1

Supporting Quantified Statements, Part 2

Supporting Quantified Statements, Part 3

Supporting Quantified Statements, Part 4

Supporting Quantified Statements, Part 5

Fixing Loops

Supporting Loop Invariants

Ad Hoc Ghosts and Loop Variants

Loops and Quantified Statements

Licensing and Download

Formal Methods Toolkit packages are available in two variants:

• GPL package: General Public License, version 3, intended for product evaluation and educational projects, which do not need to rely on dedicated technical support. This package is not intended for commercial and safety-critical systems.
• Professional package: Intended for use in commercial and safety-critical projects, which can benefit from dedicated technical support. Contact us for details.

Questions?

Need more information about the FMT project? Do not hesitate to ask.