Postdoctoral Fellow

Chair for Logic and Verification

Technical University of Munich

zhan@in.tum.de

I am working on automation techniques in interactive theorem proving, both for formalization of mathematics and for verification of computer programs.

- Project home page for auto2: https://github.com/bzhan/auto2
*(with Maximilian P. L. Haslbeck)*Verifying asymptotic time complexity of imperative programs in Isabelle.*IJCAR 2018*arXiv repository- Efficient verification of imperative programs using auto2.
*TACAS 2018*arXiv slides - Formalization of the fundamental group in untyped set theory using auto2.
*ITP 2017*arXiv slides - AUTO2, a saturation-based heuristic prover for higher-order logic.
*ITP 2016*arXiv slides

- Python code for computations in bordered Floer homology: https://github.com/bzhan/bfh_python
- Combinatorial proofs in bordered Heegaard Floer homology.
*Algebr. Geom. Topol.*16 (2016) 2571-2636 arXiv published version - Explicit Koszul-dualizing bimodules in bordered Heegaard Floer homology.
*Algebr. Geom. Topol.*16 (2016) 231-266 arXiv published version