Shenghao YUAN Researcher Email: shenghao.yuan@inria.fr / nuaaysh@126.com Software: GitLab / GitHub

---

[ Eduation ] [ Research ] [ Publications ]

---

Eduation

• Undergraduate. Sept.2013 - Jun.2017, Software Engineering
  • College of Computer Science and Technology (CCST), Nanjing University of Aeronautics and Astronautics (NUAA), China
• Master. Sept.2017 - Apr.2020, Software Engineering
  • College of Computer Science and Technology (CCST), Nanjing University of Aeronautics and Astronautics (NUAA), China
• PhD. Sept.2020 - Dec.2023, Computer Science
  • The Time, Events and Architectures(TEA) team, Université de Rennes/ Inria-Rennes, Franch

---

Research Interests

I am interested in theorem proving (Coq and Isabelle/HOL), compiler/OS formal verification. Especially, Linux eBPF-related verification~

Current Research

• Compiler Verification (CompCert-related)
  • From Coq to C [CAV2022]
  • JIT (Just-In-Time) Compiler [CAV2024]
• OS/VM Verification
  • RIOT-OS rBPF VM [MIDDLEWARE2022]
  • Linux eBPF
  • seL4
• Model-driven development
  • AADL/ Synchronous Lanuage [SCP2021]

---

Selected Publications [DBLP] [Google Scholar]

• CAV2024: End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT (Conditional Accept)
  Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
  In 36th International Conference on Computer-Aided Verification (CCF-A conf)
• SETTA2023/JSA2024: Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
  Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin
  In Symposium on Dependable Software Engineering: Theories, Tools and Applications (CCF-C conf)
  (An invited extension to Journal of Systems Architecture, CCF-B journal)
  
• CAV2022: End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
  Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli
  In 34th International Conference on Computer-Aided Verification (CCF-A conf)
• SCP2021: Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study
  Zhibin Yang, Shenghao Yuan, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, Yong Zhou
  Science of Computer Programming (CCF-B journal)

---

Visitors: