Chair for Logic and Verification
Technical University of Munich
I am working on automation techniques in interactive theorem proving,
both for formalization of mathematics and for verification of computer
- Project home page for auto2:
- Efficient verification of imperative programs using auto2.
- Formalization of the fundamental group in untyped set theory using auto2.
- AUTO2, a saturation-based heuristic prover for higher-order logic.
During graduate school, I did research in low dimensional topology, in
particular Heegaard Floer homology.