Bin Fang
Bin Fang a research engineer at Huawei. He got his joint-Ph.D. in computer science from Paris Université Paris Cité and East China Normal University (ECNU), and was supervised by Prof. Ahmed Bouajjani, Prof. Mihaela Sighireanu and Prof. Geguang Pu. His research interests center on system safety and security, formal verification, abstract interpretation, trustworthy AI system, etc.
Projects
AI-Assisted R&D
Exploring Formal Specification guided AI-assisted software development paradigm
AI Safety
Exploring Agent safety mechanisms including dynamic permission control and runtime security
HarmonyOS Kernel/TEE Formal Verification Project Manager · Architect · SE
Large-scale automated formal verification for OS kernels. Developed verification tools and program analysis platforms. Published at CAV. Presented at Huawei HDC Keynote
HarmonyOS Kernel EAL5+/EAL6+ Security Certification Project Manager · Security Engineer · Formal SE
Led formal verification engineering for CC EAL5+ and EAL6+ certification. Built formal proof platform evaluated by European certification body. Enabled HarmonyOS to achieve first commercial OS CCEAL6+ certification
HarmonyOS Kernel ISO 26262 Functional Safety Certification Project Manager · Safety Manager · TUV Certified Safety Engineer
Managed end-to-end functional safety certification. Established ISO 26262 software product certification process. Achieved ASIL-D certification
Program Analysis & RTOS Formal Verification Core Developer
Developed static analysis tools based on abstract interpretation (heap-manipulating programs, pointer arithmetic, memory safety). Participated in RTOS formal verification in collaboration with J.-R. Abrial (European Academy of Sciences)
Work Experience
Principal Engineer · Security Expert · Tech Manager
Huawei · Shanghai
Industry Ph.D. Supervisor at Shanghai Jiao Tong University
Senior Engineer · Project Lead & Manager
Huawei · Shanghai
Joint Training Manager (Transportation-Huawei)
Teaching Assistant
East China Normal University · Shanghai
Graduate Program Analysis Course
Research Intern
Shanghai Key Lab of Trustworthy Computing · Shanghai
Education
Joint Ph.D. (China-France)
Paris Cite University & East China Normal University · Computer Science · Formal Verification
Advisors: Prof. Geguang Pu, Prof. Ahmed Bouajjani, Prof. Mihaela Sighireanu
Ph.D. Student
East China Normal University · Software Engineering Theory and Technology
Bachelor
East China Normal University · Software Engineering
Publications
-
1.
Enabling Semantic Evolutionary Analysis of Application via High-Precision Binary Diffing Under Submission, 2026
-
2.
AgentVerify: Compositional Formal Verification of AI Agent Safety Properties via LTL Model Checking Preprint, 2025
-
3.
Affine Loop Invariant Generation via Matrix Algebra The 34th International Conference on Computer Aided Verification (CAV), 2022
-
4.
Formal modelling of list based dynamic memory allocators SCIENCE CHINA Information Sciences, 2018
-
5.
A refinement hierarchy for free list memory allocators ACM SIGPLAN International Symposium on Memory Management (ISMM), 2017
-
6.
Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2016
-
7.
Formal Development of a Real-Time Operating System Memory Manager International Conference on Engineering of Complex Computer Systems (ICECCS), 2015
-
8.
Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution International Conference on Software Security and Reliability (SERE), 2014
-
9.
Runtime Verification by Convergent Formula Progression Asia-Pacific Software Engineering Conference (APSEC), 2014
Honors & Awards
China National Scholarship for International Doctorate
2014-2018 · France
Marktoberdorf Summer School Scholarship
2017 · Germany
MOVEP Summer School Scholarship
2016 · Italy