PetriDotNet is a framework for the editing, simulation and analysis of Petri nets. Our aim is an easy to use and extendable tool to support Petri net based modelling and verification. It provides a convenient graphical editor for creating (ordinary or coloured) Petri nets. It is extended with analysis of structural and dynamic properties of Petri nets, simulation, reachability and model checking capabilities.


For more information on the VIATRA2 model transformation framework, we kindly refer the reader to the VIATRA portal, the official website, and the Eclipse Wiki.

A thematic list of VIATRA2-related publications is available here. A comprehensive list is available on the portal.


EMF-IncQuery is an Eclipse-based framework that supports high-performance incremental model queries over large instance models. Based on the incremental graph pattern matching engine, core model-driven engineering applications such as on-the-fly well-formedness validation, model synchronization and view maintenance can be easily implemented in an extremely scalable way. More information is available on the official website of the project.

Gamma Statechart Composition Framework

The Gamma Statechart Composition Framework is a modeling framework to model, verify and generate code for component-based reactive systems, developed at the Critical Systems Research Group of Budapest University of Technology and Economics.

Gamma Statechart Composition Framework Read more »

Theta: a Framework for Abstraction Refinement-Based Model Checking

Theta is a generic, modular and configurable model checking framework developed at the Fault Tolerant Systems Research Group of Budapest University of Technology and Economics, aiming to support the design and evaluation of abstraction refinement-based algorithms for the reachability analysis of various formalisms.