What follows is aimed at theoretical computer scientists in the field of formal machine-aided verification of software or hardward properties.
I have implemented model checker Alfred in C++/STL as part of my master's thesis at the Faculty of Informatics (should be Computer Science, but that is how they call themselves in English) at Masaryk University, Brno. The model checker decides the validity of formulas of alternation free modal mu-calculus for push down systems, and push down automata. Also available is the source code of the model checker. The model checker implements the algorithm described in article Reachability Analysis of Pushdown Automata: Application to Model-Checking. Modal Mu-calculus is a temporal logic with fixed point operators, of branching time, as opposed to a linear-time logic like LTL.
External links: