Model Checking Unleashed
This project aims at using model checking techniques in order to tackle all sorts of other decision and computation problems. It is funded by the European Research Council in form of an Independent Starting Researcher Grant over the course of 5 years.


VeriNonReg, Verification of Non-Regular Properties
This project aims to extend the scope of automatic program verification to structurally more complex properties, namely non-regular languages of words and trees. It was funded by the Deutsche Forschungsgemeinschaft for 3 years, and employed PhD student Roland Axelsson.


PGSolver
The PGSolver library is a collection of algorithms for solving parity games that appear somewhere in the literature, as well as some new heuristics etc. It also defines a standard specification format for parity games as well as winning regions and strategies, and provides a collection of benchmark games. Co-developer of this tool is Oliver Friedmann.


MLSolver
MLSolver is a tool for deciding validity and satisfiability of temporal logics, mainly branching-time logics. It uses tableau and automata techniques and reductions to parity games which are solved using PGSolver mentioned above. Main developer of this tool is Oliver Friedmann.


CFGAnalyzer
A tool that analyzes context-free grammars w.r.t. certain undecidable problems: universality, language inclusion, equivalence, intersection, and ambiguity. It uses an incremental SAT solver to implement semi-decision procedures - not an approximation, i.e. the answers are sound and complete but the program may not terminate. It is described in a paper with Roland Axelsson and Keijo Heljanko.