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 0.118 - for build instructions we refer to the file contained in the archive.

Binaries are also available for

  • macOS (64 bits architecture, tested under macOS 10.13.6 - High Sierra)
  • Linux (x86_64 architecture, tested under Debian Wheezy

Selected case studies and ProFeat model files can be found 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.