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 (Wayback Machine). Modal Mu-calculus is a temporal logic with fixed point operators, of branching time, as opposed to a linear-time logic like LTL.
The master's thesis has the title "Verifying Properties of Infinite-state Systems" and was "published" in 2000, Masaryk University; it is attached below. The thesis seems to be referenced from the following (see also Google Scholar search):
Compositional Verification for Secure Loading of Smart Card Applets , Christoph Sprenger, Dilian Gurov, Marieke Huisman, 2004
Checking Absence of Illicit Applet Interactions: A Case Study, Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov, 2004
Compositional verification of sequential programs with procedures, Dilian Gurov, Marieke Huisman, Christoph Sprenger, 2008
Programmanalysen zur Verbesserung der Softwaremodellprüfung, doctoral thesis, Dirk Richter, 2012.
External links: