Gemini: A Lightweight Virtualization Architecture for Protecting Privacy and Security of Smartphone. - Shichao Liao; Xia Yang; Wensheng Guo; Haiyong Sun; Zhixiang Jiang; Xiaoyan Zhao (ICESS, 2016)

A Fast Boot, Fast Shutdown Technique for Android OS Devices. - Xia Yang; Peng Shi; Haiyong Sun; Wenxuan Zheng; Jim Alves-Foss (Computer, 2016)

Formal Verification of GP Specification based Embedded Operating System. - Haiyong Sun; Hang Lei; Lei Qiao; Zheng Yang 007 (CSAE, 2018)

针对RTOS的轻量级强制访问控制技术的研究与实现 (Research and Implementation of Light-weight Mandatory Access Control Technology for RTOS). - Xia Yang; Shan Yang; Wensheng Guo; Haiyong Sun; Xiaoyan Zhao; Yang Zhang (计算机科学, 2018)

A Design and Verification Methodology for a TrustZone Trusted Execution Environment. - Haiyong Sun; Hang Lei (IEEE Access, 2020)

Formal verification of a task scheduler for embedded operating systems. - Haiyong Sun; Hang Lei (J. Intell. Fuzzy Syst., 2020)

Automatic Generation of Formal BIP Models for C Programs. - Qiming Li; Xia Yang; Haiyong Sun; Zhe Yan (CSAE, 2023)