Tools

Current Tools

The following software tools have been developed by the FMT group over the recent years. We are still working on these tools and invite you to experiment with them.

• The Modest Toolset: Quantitative Modelling and Analysis
• VerCors : Verification of Concurrent Data Structures
• ANIMO: Analysis of Networks with Interactive MOdeling
• GROOVE: Graph Transformation, State Space Exploration and Verification
• JTorX: a Tool for Model-Based Testing
• FFORT: A benchmark suite for Fault Tree Analysis
• Lace: efficient work-stealing implementation in C
• LTSmin: Minimization and Instantiation of Labelled Transition Systems
• Puptol: Publish Your (Prototype) Tool On-Line
• SCOOP: Symbolic reductions of probabilistic specifications with data
• SpinJa: A model checker for Promela, written in Java
• Sylvan: parallel BDDs
• DFTCalc: Dynamic Fault Tree Calculator

Legacy Tools

Below you can find several tools that have been developed by the FMT group, but that are not longer actively maintained and supported. You are still welcome to use these older tools, though.

• Bhave: Simulation of Hybrid Systems
• IMCA: Interactive Marcov Chain Analyzer (replaced by Storm)
• kimwitu: A Term Processor
• LITE: LOTOS Integrated Tool Environment
• MoonWalker: A Model Checker Developed on the Mono Platform
• MoTor: MoDeST Tool Environment
• MRMC: Markov Reward Model Checker
• ProMoVer: A Tool for Procedure-Modular Verification
• SLADE: Student LAnguage Development Environment
• TorX: a Tool for Model-Based Testing
• TorXviz: an approach to visualization (used by TorX and JTorX)