About ME
wechat: yuezhuangwenzi
Profile
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.
Education
| 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 |
Papers
| 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. |
web |
Awards
| 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 |
Skills
| Type | Languages |
|---|---|
| Programming | OCaml |
| Formalisation /Verification | Event-B / VCC / Frama-c / Coq … |
| other | … |
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