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:
- (with Maximilian P. L. Haslbeck) Verifying asymptotic time complexity of imperative programs in Isabelle.
- 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.