Projects

• 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 is Martin Lange.

• MLSolver
  The MLSolver library is a collection of algorithms for solving the satisfiability and validity problems for modal fixpoint logics. It also defines a standard specification format for transition systems, a macro language for defining families of formulas and provides a collection of benchmark problems. Co-developer is Martin Lange.

• FADecider
  A package for deciding universality and subsumption of omega automata using Ramsey-based methods. Co-developers are Felix Klaedtke and Martin Lange.

• TCSLib
  A multi-purpose library for OCaml. Co-developer is Martin Lange.

• CamlDiets
  A highly efficient set implementation for fat sets, i.e. densely populated sets over a discrete linear order. Our source code is written in OCaml and implements the Set-interface. Co-developer is Martin Lange.

• SATSolversForOcaml
  A library for integrating SAT Solvers into OCaml. Co-developer is Martin Lange.

• MetapostGraphs
  A library that allows you to draw graphs using metapost and latex. Co-developer is Thomas D. Hansen.

• Parity Game SAT Benchmarks
  Benchmarks that originate from my research investigating the structure of the strategy improvement algorithm for parity games; used in the crafted category of the SAT competition, 2009.