Christian Dax Email: firstname.lastname@gmx.de (pgp-key)

In 2010, I left academia to find new challenges in industry.
I studied computer science at the University of Munich and University of Edinburgh and did my PhD in David Basin's group at the ETH in Zürich. My supervisor was Felix Klaedtke.

Tools

1. [ psl2ba tool ] Translator for PSL specifications, i.e., LTL + regular expressions + past operators, to nondeterministic Büchi automata.
2. [ WDBA tool ] Optimizing finite-state model checking using weak deterministic Büchi automata. For further details, see our ATVA'07 paper.

Publications

1. On Regular Temporal Logics with Past
   Acta Informatica 2010 paper with Felix Klaedtke and Martin Lange
   [ pdf ]
    
2. Specification Languages for Stutter-Invariant Regular Properties
   ATVA 2009 paper with Felix Klaedtke and Stefan Leue
   [ pdf | bib | slides]
    
3. On Regular Temporal Logics with Past
   ICALP 2009 paper with Felix Klaedtke and Martin Lange
   [ pdf | bib | slides | psl2ba tool ]
    
4. Alternation Elimination by Complementation
   LPAR 2008 paper with Felix Klaedtke
   [ pdf | bib | slides | slides2 | slides3 ]
    
5. Mechanizing the Powerset Construction for Restricted Classes of omega-Automata
   ATVA 2007 paper with Jochen Eisinger and Felix Klaedtke
   [ pdf | bib | slides | WDBA tool | experiments ]
    
6. LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
   CAV 2007 paper with Bernd Becker, Jochen Eisinger, and Felix Klaedtke
   [ pdf | bib | LIRA tool ]
    
7. A Proof System for the Linear Time mu-Calculus
   FSTTCS 2006 paper with Martin Hofmann and Martin Lange
   [ pdf | bib | slides ]
    
8. Game Over: The Foci Approach to LTL Satisfiability and Model Checking
   GDV 2004 paper with Martin Lange
   [ pdf | bib ]

Thesis/Technical Reports

1. From Temporal Logics to Automata via Alternation Elimination. PhD Thesis, ETH Zurich, 2010.
   [ pdf | slides ]
    
2. Mechanizing the Powerset Construction for Restricted Classes of omega-Automata. Technical Report with Jochen Eisinger and Felix Klaedtke: Institut für Informatik, Universität Freiburg, 2007.
   [ bib | pdf ]
    
3. Games for the Linear Time mu-Calculus. Master's thesis, Dep. of Computer Science, University of Munich, 2006.
   [ bib | slides | pdf ]
    

Theaching

1. Model Checking HS 2009: homepage
2. evim FS 2008: homepage
3. Information Security FS 2008: slides
4. Logic HS 2007: slides
5. Information Security FS 2007
6. Logic HS 2006

Any comments? Mail me at firstname.lastname@gmx.de