Inspirel banner

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:

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:

Gallery

Documentation

FMT book cover

"Formal Methods Toolkit" by Maciej Sobczak

This book is a complete FMT manual that describes its features and usage patterns.

Support independent publishing: Buy this book on Lulu.

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.

Development blog

The articles linked below document the reasoning behind new FMT features.

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

Licensing and Download

Formal Methods Toolkit packages are available in two variants:

Package:

Purpose:

FMT-gpl-1.0.zip

Wolfram source packages with example Mathematica notebook files.

Questions?

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