wechat: yuezhuangwenzi


I am now a senior research engineer and project leader of formal verification team in OS kernel lab at Huawei since 2019. I finished my Ph.d as a joint-Ph.d between East China Normal University and Université Paris Diderot under supervision of Geguang Pu, Ahmed Bouajjani and Mihaela Sighireanu. My research interests are formal modelling and verification, refinement and abstract interpretation. And I am working on enhancing adoption of formal methods using in software industry. Please do not hesitate to contact me if you want to join us or have cooperation.


Time Place Title
Sep 2014 - Jul 2018 Université Paris Diderot & East China Normal University Ph.D of Computer Science, Program Verification
Sep 2013 - July 2014 East China Normal University Master, Software Engineering
Sep 2010 - Jun 2013 East China Normal University Bachelor, Software Engineering

Experience & Project

Time Role Content
2015-2017 Paris Phd project, Static Analyzer Built Mman (in OCaml), a static analyzer for heap-maniplulating programs based on Abstract Interpretation, Formal verification for categories of memory models
2014 Shanghai Teaching Assistants Tools of Program Analysis, Testing, and Verification 2014 Semester 1, ECNU
2014 Shanghai Program Analysis Intern Shanghai Key Laboratory of Trustworthy Computing
2013-2014 Beijing, Shanghai Researcher, System modeling and Verification Formal verified components of real time operating system developed by Beijing Institute of Control Engineering


Year Paper pdf, link
2022 Affine Loop Invariant Generation via Matrix Algebra
Yucheng Ji, Hongfei Fu, Bin Fang and Haibo Chen, CAV2022
2018 Techniques for Formal Modelling and Verification on Dynamic Memory Allocators.
Bin Fang, Ph.D thesis,
pdf, slides
2017 Formal Modelling of List Based Dynamic Memory Allocators.
Bin Fang, Mihaela Sighireanu, Journal of SCIENCE CHINA Information Sciences, 2017,
pdf, web
2017 A Refinement Hierarchy for Free List Memory Allocators.
Bin Fang, Mihaela Sighireanu. ACM SIGPLAN International Symposium on Memory Management (ISMM) 2017.
2016 Hierarchical Shape Abstraction of Free-List Memory Allocators.
Bin Fang, Mihaela Sighireanu. 26th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR 2016.
pdf, web
2015 Formal Development of a Real-Time Operating System Memory Manager.
Wen Su, Jean-Raymond Abrial, Geguang Pu, Bin Fang. 20th International Conference on Engineering of Complex Computer Systems ICECCS 2015.
pdf, web
2014 Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution.
Ting Su, Siyuan Jiang, Geguang Pu, Bin Fang, Jifeng He, Jun Yan, Jianjun Zhao. Eighth International Conference on Software Security and Reliability, SERE 2014.
pdf, web
2014 Runtime Verification by Convergent Formula Progression.
Yan Shen, Jianwen Li, Zheng Wang, Bin Fang, Geguang Pu and Wangwei Liu. 21st Asia-Pacific Software Engineering Conference APSEC 2014.


Time Scholarship
Oct 2014 - Oct 2018 China National Scholarship for International Doctorate
Jul 2017 Travel grant and registration waiver to Marktoberdorf School
Jul 2016 Travel grant and registration waiver to MOVEP School


Type Languages
Programming OCaml
Formalisation /Verification Event-B / VCC / Frama-c / Coq …

This blog is the place in which I put my literature writing (almost in Chinese) that records the feeling of every moment in my life and technical articles for popular science including algorithm, programming and verification theory.

SLAM, Frama-c, CBMC, KLEE, LLVM, Z3, Event-B, IRIF lab, SSEL lab

いしかわ たくぼく

只要想起一生中后悔的事 梅花便落满了南山

Le Mythe de Sisyphe (Albert Camus)

The Art of Loving (Erich Fromm)