Tools

A framework for decision diagrams written in Rust. Supports safe, concurrent, modular, and performant decision diagram construction. EASST best paper award.

Main developer:  Nils Husung

Computes causes for outcomes of Boolean functions, providing partial interpretations — so-called feature causes — from propositional logic formulas.

An explicit CTL model checker for recursive state machines using lazy evaluation to speed up analysis.

Main developer:  Patrick Wienhöft

A language and tool for describing and analyzing (probabilistic) feature-oriented systems and software product lines. Generates compositional family models in Prism language.

Main developer:  Philipp Chrszon

A Java tool for quantitative message sequence graphs (qMSGs), enabling model checking of CSL properties for compositional qMSGs. Contact me if you are interested.