Associate Researcher

State Key Laboratory of Computer Science

Institute of Software, Chinese Academy of Sciences

bzhan@ios.ac.cn

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

Journal Articles:

- Formalization of the fundamental group in untyped set theory using auto2.
*JAR 2018*published version

Conference Papers:

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

Other talks:

- Proof automation in set theory.
*Conference in honour of Thomas C. Hales on the occasion of his 60th birthday.*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