Game Over: The Foci Approach to LTL Satisfiability and Model Checking. - Christian Dax; Martin Lange (GDV@CAV, 2004)

A Proof System for the Linear Time µ-Calculus. - Christian Dax; Martin Hofmann 001; Martin Lange (FSTTCS, 2006)

Mechanizing the Powerset Construction for Restricted Classes of omega -Automata. - Christian Dax; Jochen Eisinger; Felix Klaedtke (ATVA, 2007)

LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. - Bernd Becker 001; Christian Dax; Jochen Eisinger; Felix Klaedtke (CAV, 2007)

Alternation Elimination by Complementation (Extended Abstract). - Christian Dax; Felix Klaedtke (LPAR, 2008)

Specification Languages for Stutter-Invariant Regular Properties. - Christian Dax; Felix Klaedtke; Stefan Leue (ATVA, 2009)

On regular temporal logics with past. - Christian Dax; Felix Klaedtke; Martin Lange (Acta Informatica, 2010)

Alternation Elimination for Automata over Nested Words. - Christian Dax; Felix Klaedtke (FoSSaCS, 2011)