Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study. - Shenghao Yuan; Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Tiexin Wang; Yong Zhou (FTSCS, 2019)

Verified functional programming of an IoT operating system's bootloader. - Shenghao Yuan; Jean-Pierre Talpin (MEMOCODE, 2021)

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 (Sci. Comput. Program., 2021)

End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. - Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin; Samuel Hym; Koen Zandberg; Emmanuel Baccelli (CAV (2), 2022)

Femto-containers: lightweight virtualization and fault isolation for small software functions on low-power IoT microcontrollers. - Koen Zandberg; Emmanuel Baccelli; Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin (Middleware, 2022)

Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification. - Shenghao Yuan; Benjamin Lion; Frédéric Besson; Jean-Pierre Talpin (SETTA, 2023)

Verified programming and secure integration of operating system libraries in Coq. (Programmation vérifiée et intégration sécurisée de bibliothèques de systèmes d'exploitation dans Coq). - Shenghao Yuan (2023)

End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT. - Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin (CAV (1), 2024)

Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. - Jiayi Lu; Shenghao Yuan; David Sanán; Yongwang Zhao (SETTA, 2024)

A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana. - Shenghao Yuan; Zhuoruo Zhang; Jiayi Lu; David Sanán; Rui Chang; Yongwang Zhao (Proc. ACM Program. Lang., 2025)