Tools
OxiDD is a framework for decision diagrams written in Rust. It has been first presented in the TACAS'24 publication " OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust".More information about the tool and experimental data can be found at oxidd.net.
FeatCause is a tool to compute causes for outcomes of Boolean functions, providing partial interpretations -- so-called feature causes -- from propositional logic formulas for effects and valid interpretations. The underlying algorithm has been presented in the ICSE'22 publication about "Causality in Configurable Software Systems".
More information about the tool and experimental data can be found at GitHub.
RSMCheck is an explicit CTL model checker for recursive state machines. It uses a lazy evaluation scheme to speed up the analysis by only evaluating components when they could contribute to the overall (un)satisfaction of the formula. Evaluation of the performance is presented in the SEFM'21 publication. The main developer of RSMCheck is Patrick Wienhöft.
More information about the tool and download options can be found at GitHub.
ProFeat is developed at TU Dresden and is both, a language and a tool. It can be used to describe and analyze (probabilistic) feature-oriented systems such as (probabilistic) software product lines. But it is also useful for non-featured family-based analysis and as an extension of the input language of the probabilistic model checker Prism by supporting arrays and simple for-loops. It fully covers the modeling framework for feature-oriented systems presented in the Modularity'14 paper and can generate compositional family models in Prism language (at least for the parallel feature composition according to the SEFM'19 publication). The main developer of ProFeat is Philipp Chrszon.
More information about the tool and download options can be found at GitHub.
aMeSGee is a tool written in Java I developed for the FORMATS'15 publication about quantitative message sequence graphs (qMSGs). It enables model checking CSL properties even for compositional qMSGs. Please contact me if you are interested in the program. As the underlying semantics also provides a transition-system semantics, this implementation can also be useful for (bounded, non-probabilistic) model checking of MSGs. See also this publication about delayed-choice semantics of MSGs.