CLTSA (Counting Fluents Labelled Transition System Analyser) is an extension of LTSA (Labelled Transition System Analyser) that incorporates counting fluents, a useful mechanism to capture properties related to counting events. The tool supports a superset of FSP, that allows one to define properties involving counting fluents, which the tool can also model check.

Check out the tool demo!

DynAlloy is a formal specification language that extends Alloy (a formal specification language based on first-orded logic and relational operations including transitive closure), by incorporating actions and programs, to better describe state change and properties of state changing situations. DynAlloy Analyzer is a tool for DynAlloy specification, built over Alloy Analyzer, that supports fully automated and efficient analysis of DynAlloy specifications, resorting to SAT solving.

Check out the tool demo!

BEAPI is an efficient bounded exhaustive test generation tool that employs routines from the API of the software under test for generation. BEAPI solely employs the public methods in the API of a class in order to perform bounded exhaustive input generation for the class, without the need for a formal specification of valid inputs.