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:
- Formalization of the fundamental group in untyped set theory using auto2.
- Automation of separation logic 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.