Collection of resources for research concerning Machine Learning and Formal Methods.

The Termination Problem Database

JKind - a Java implementation of the KIND model checker

JKind - An infinite-state model checker for safety properties in Lustre

Decision Tree Learning Algorithm for Reactive Synthesis

The Stately FSM design tool.

Ranking Functions Finder

A tool for reachability and termination analysis of integer programs

Reads a state transition system and performs property checking

Here we collect worldwide courses teaching formal methods

Links to tools by subject

Bounded synthesis via safety games and BDDs

UCLID5: formal modeling, verification, and synthesis of computational systems

A tool for reactive synthesis with monitor triggers.

A toolkit for modelling and verification of reconfigurable multi-agent systems.

Program analysis playground for a simple, imperative language

The Ultimate program analysis framework.

[⚠ Looking for a new maintainer] Parity UI - The Parity Dapp shell, browser & launcher (Electron app)

A tool for obtaining LTL formulas from a sample of positive and negative words.

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces

Strix is a tool for reactive synthesis of controllers from LTL specifications.

SmalL bUt Complete GROne Synthesizer

A toolkit for designing and implementing LTL-based task specifications.

GitHub Action to compile LaTeX documents

Prototype compiler from AWS CloudFormation IaC templates into Logic.

LTL3TELA is a translator of LTL formulae to omega-automata with generic acceptance condition.

Symbolic execution tool