University Paris Diderot - Paris 7
Laboratory IRIF
Sophie Germain, 4061
+33 (0) 7 68 79 02 80
wechat: ericbinder
bfang@irif.fr
http://bfang.info
linkedin

Profile

I am a Ph.D candidate (will graduate Sep. 2018) in joint-Ph.d program between East China Normal University and Université Paris Diderot. My research interests are operating system verification, refinement and static analysis based on abstract interpretation. And I am working on enhancing adoption of formal methods using in software industry. I am under supervision of Prof. Geguang Pu in Shanghai, Prof. Ahmed Bouajjani and Dr. Mihaela Sighireanu in Paris.

keywords

Static Analysis, Symbolic Execution, Program Verification, Software Reliability

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
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 Verified components (memory manager, etc) of real time operating system developed by Beijing Institute of Control Engineering

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 C / C++ / Java / Python / OCaml / SQL / CSS / HTML / Javascript / PHP / etc
Formalisation /Verification Event-B / VCC / Frama-c / CVIL / SMT / Z3/ CIL / etc
other Git / Latex / Rodin / etc

Papers

Year Paper pdf, link
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.
pdf
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

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)