ProFeat is a tool developed at TU Dresden that provides a feature-oriented modeling language to describe families of probabilistic systems and a framework that enables the feature-aware analysis of such families using state-of-the-art probabilistic model checkers.

Quick start

Download the source code of ProFeat - for build instructions we refer to the file contained in the archive.

Binaries are also available for

  • macOS (64 bit architecture, tested using macOS 10.14.4)
  • Linux (x86_64 architecture, tested using Debian Stretch)

An AUR package is available as well.

For information on the usage of ProFeat, we refer to the documentation.

The source code of ProFeat (the version used in the publications) is also available.

Selected case studies and ProFeat model files can be downloaded here.


  • Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier
    ProFeat: Feature-oriented Engineering for Family-based Probabilistic Model Checking
    Formal Aspects of Computing, volume 30(1), pp 45-75, 2018. Link.

  • Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier
    Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat
    Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE’16),
    Lecture Notes in Computer Science 9633, pp 287-304, 2016, (best paper award nomination). Link, additional material.

Other publications using ProFeat

  • Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich
    Greener Bits: Formal Analysis of Demand Response
    Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16),
    Lecture Notes in Computer Science 9938, pp 323-339, 2016.


This page was built with Hugo using the Material theme.