主要论著 Selected Publication (# Corresponding Author) [所有论文见 DBLP Records ]
  1. [OOPSLA 2025] Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, Yongwang Zhao, "A complete formal semantics of eBPF instruction set architecture for Solana", ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2025) , accepted (CCF A) [PDF download]
  2. [TOPLAS 2021] David Sanan, Yongwang Zhao#, Yang Liu, Shangwei Lin, "CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee", ACM Transactions on Programming Languages and Systems (TOPLAS) , Vol. 43, No. 1, February 2021, pp. 2:1 - 2:46 (CCF A) [PDF download]
  3. [TOSEM 2025] Jianhong Zhao, Yongwang Zhao#, Peisen Yao, Fanlang Zeng, Bohua Zhan, and Kui Ren, "KBX: Verified Model Synchronization via Formal Bidirectional Transformation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 34, Issue 2, Article No. 43, January 25, 2025, Pages 1 - 40 (CCF A)
  4. [TDSC 2024] Jilin Hu, Fanlang Zeng, Yongwang Zhao#, Zhuoruo Zhang, Leping Zhang, Jianhong Zhao, Rui Chang, and Kui Ren, "ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile", IEEE Transactions on Dependable and Secure Computing (TDSC), Volume 21, Issue 6, November/December 2024, pp. 5341 - 5358 (CCF A)
  5. [TDSC 2023] Xinliang Miao, Rui Chang, Jianhong Zhao, Yongwang Zhao, Shuang Cao, Yulong Zhang, Tao Wei, Liehui Jiang, and Kui Ren, "CVTEE: A Compatible Verified TEE Architecture with Enhanced Security", IEEE Transactions on Dependable and Secure Computing (TDSC), Volume 20, Issue 1, 01 Jan.-Feb. 2023, pp. 377 - 391 (CCF A)
  6. [FM 2021] Wenjing Xu, Yongwang Zhao#, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang and Shihong Zou, "Apply Formal Methods in Certifying the SyberX High-Assurance Kernel", In Proceedings of 24th International Symposium on Formal Methods (FM 2021) , 20-26 November, 2021, Beijing, China, pp. 788 - 798. [PDF download] (CCF A)
  7. [FM 2019] Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu, "A Parametric Rely-guarantee Reasoning Framework for Concurrent Reactive Systems", 23rd International Symposium on Formal Methods (FM 2019), Oct 7-11, 2019, Porto, Portugal, pp. 161-178 (CCF A)[PDF download]
  8. [CAV 2019] Yongwang Zhao, David Sanan, "Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS", 31st International Conference on Computer-Aided Verification (CAV 2019), July 15-18, 2019, New York City, NY, USA, pp. 515-533 (CCF A)[PDF download]
  9. [TDSC 2019] Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu, "Refinement-based Specification and Security Analysis of Separation Kernels", IEEE Transactions on Dependable and Secure Computing (TDSC), Volume 16, Issue 1, January 2019, pp. 127 - 141 (CCF A) [PDF download]
  10. [FM 2018] Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-wei Lin, Jun Sun, "Compositional Reasoning for Shared-variable Concurrent Programs", 22nd International Symposium on Formal Methods (FM 2018), 15-17 July 2018, Oxford UK, pp. 523-541 (CCF A) [PDF download]
  11. [SCIS 2024] 古金宇, 李浩, 夏虞斌, 管海兵,丁佐华, 赵永望, 陈海波. BrickOS: 面向异构硬件资源的积木式内核. 中国科学: 信息科学, 2024, 54: 491–513. (CCF A) [PDF download]
  12. [TACAS 2024] Leping Zhang, Yongwang Zhao#, Jianxin Li, "A Comprehensive Specification and Verification of the L4 Microkernel API", 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024, ETAPS), Luxembourg City, Luxembourg, 6–11 April 2024, pp. 217 - 234 (CCF B, Top conf. in formal methods) [PDF download]
  13. [STVR 2025] Feng Zhang, Yongwang Zhao#, Yang Liu, Jun Sun, "A Comprehensive Formal Specification of ARINC 653 with Conformity Proof", Software Testing, Verification and Reliability (STVR), Volume 35, Issue 1, January 2025, pp. 1 - 17 (CCF B) [Link]
  14. [FCS 2024] Jinhui Kang, Jianhong Zhao, Yongwang Zhao#, "K-SELinux: Formal Analysis and Verification of SELinux Policies via Semantic Execution", Frontiers of Computer Science, 2024, pp. XXX - YYY (Accepted) (CCF B)
  15. [FCS 2017] Yongwang Zhao, Zhibin Yang, Dianfu Ma, "A survey on formal specification and verification of separation kernels", Frontiers of Computer Science , Volume 11, Issue 4, August 2017, pp. 585 – 607. [PDF download] (CCF B)
  16. [TACAS 2016] Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu, "Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication", 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016, ETAPS), 2-8 April 2016, Eindhoven, The Netherlands, pp. 791-810 (CCF B, Top conf. in formal methods) [PDF download]
  17. [FAC 2023] Feng Zhang, Leping Zhang, Yongwang Zhao#, Yang Liu, Jun Sun, "Refinement-Based Specification and Analysis of Multi-Core ARINC 653 Using Event-B", Formal Aspects of Computing, Volume 35, Issue 4, November, 2023, Article No.24, pp 1–29. (CCF B) [PDF download]
  18. [FCS 2021] Shahbaz Ali, Hailong Sun, Yongwang Zhao#, "Model Learning: A Survey on Foundation, Tools and Applications", Frontiers of Computer Science, Volume 15, Issue 5, October 2021, pp. 1 - 22. [PDF download] (CCF B)
  19. [TACAS 2017] David Sanan, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu, "CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs", 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, ETAPS), 22-29 April 2017, Uppsala, Sweden, pp. 481-498 (CCF B, Top conf. in formal methods) [PDF download]
  20. [ISSRE 2015] Yongwang Zhao, Zhibin Yang, David Sanan, Yang Liu, "Event-based Formalization of Safety-critical Operating System Standards", 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015), November 2–5, 2015, Washington DC, USA, pp. 281-292 (CCF B) [PDF download].
  21. [ISSRE 2023] Fanlang Zeng, Zhuoruo Zhang, Rui Chang, Chenyang Yu, Zijun Zhang, Yongwang Zhao, "Lark: Verified Cross-Domain Access Control for Trusted Execution Environments", 34th IEEE International Symposium on Software Reliability Engineering (ISSRE 2023), Florence, Italy, October 9 - 12, 2023, pp. 160 - 171 (CCF B) [PDF download].
  22. [ICWS 2023] Zhuoruo Zhang, Jilin Hu, Chenyang Yu, Rui Chang, Yongwang Zhao, "VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks", International Conference on Web Services (ICWS 2023) , JULY 2-8, 2023, CHICAGO, ILLINOIS USA, pp. 71 - 77. (CCF B) [PDF download].
  23. [SETTA 2024] Jiayi Lu, Shenghao Yuan, David Sanan, Yongwang Zhao, "Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness", 10th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2024) , Hong Kong, China, November 26–28, 2024, pp. 197-216. (CCF C) [PDF download].
  24. [Internetware 2023] Hao Xu, Yongwang Zhao#, "Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving", 14th Asia-Pacific Symposium on Internetware (Internetware 2023) , August 4 - 6, 2023, Hangzhou, China, pp. 313–322. (CCF C) [PDF download].
  25. [Internetware 2022] Xinliang Miao, Fanlang Zeng, Rui Chang, Chenyang Yu, Zijun Zhang, Liehui Jiang, Yongwang Zhao, "Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE", 13th Asia-Pacific Symposium on Internetware (Internetware 2022) , June 11-12, 2022, Hohhot, China, pp. 252–261. (CCF C) [PDF download]
  26. [ICFEM 2022] Ke Jiang, Tianwei Zhang, David Sanan, Yongwang Zhao, Yang Liu, "A Novel Formal Methodology for Verification of Side-channel Vulnerabilities in Cache Architectures", 23rd International Conference on Formal Engineering Methods (ICFEM 2022) , October 24-27, 2022, Madrid, Spain, pp. 190–208. (CCF C) [PDF download]
  27. 蔡少伟, 陈振邦, 王戟, 詹博华, 赵永望. "约束求解与定理证明专题前言".软件学报, 2023, 34(8):3465-3466. [PDF download]
  28. 章乐平, 赵永望#, 王布阳, 李悦欣, 冯潇潇. "L4 虚拟内存子系统的形式化验证". 软件学报, 2023年, 第34卷, 第8期. [PDF download]
  29. 曾凡浪, 常瑞, 许浩, 潘少平, 赵永望. "基于精化的TrustZone多安全分区建模与形式化验证". 软件学报, 2023年, 第34卷, 第8期. [PDF download]
  30. 曹钦翔, 詹博华, 赵永望. "定理证明理论与应用专题前言".软件学报, 2022, 33(6):2113-2114. [PDF download]
  31. 苗新亮, 常 瑞, 潘少平, 赵永望, 蒋烈辉. "可信执行环境访问控制建模与安全性分析".软件学报, 2022. [PDF download]
  32. [SETTA 2020] Yongwang Zhao, "Rely-Guarantee Reasoning About Concurrent Reactive Systems: Framework, Languages Integration and Applications (Invited Talk)", 6th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2020), November 24–27, 2020, Guangzhou, China. [PDF download] (CCF C)
  33. [TASE 2020] Wenjing Xu, Yongwang Zhao#, Dianfu Ma, Yuxin Zhang, "Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles", 14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020), December 11-13, 2020, Hangzhou, China, pp. xxx-yyy (CCF C) [PDF download]
  34. 赵永望,刘杨,王戟. "系统软件构造与验证技术专题前言".软件学报, 2020, 31(5):1241-1242. [PDF download]
  35. 李鼎基, 糜泽羽, 吴保东, 陈逊, 赵永望, 丁佐华, 陈海波, "利用跨虚拟机零下陷通信的加速器虚拟化框架", 软件学报,2020,31(10):3019-3037
  36. [ISORC 2019] Feng Zhang, Yongwang Zhao#, Dianfu Ma, Wensheng Niu, "Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS", IEEE 22nd International Symposium on Real-Time Distributed Computing (ISORC 2019), 7-9 May, 2019, Valencia, Spain, pp. 10-17.
  37. [SETTA 2019] Yu Zhang, Yongwang Zhao#, David Sanan, Lei Qiao, and Jinkun Zhang, "A Verified Specification of TLSF Memory Management Allocator using State Monads", International Symposium on Software Engineering: Theories, Tools, and Applications (SETTA 2019), Nov. 27-29, 2019, Shanghai, China, pp. 122-138. [PDF download] (CCF C)
  38. Shahbaz Ali, Hailong Sun, and Yongwang Zhao#, "Combining Model Learning and Model Checking to Analyze Java Libraries", 9th International Workshop on Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2019), Shenzhen, China, November 5, 2019, pp. 259-278.
  39. Ke Jiang, David Sanan, Yongwang Zhao, Shuanglong Kan, Yang Liu, "A Formally Verified Buddy Memory Allocation Model", 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019), 10-13 November 2019, Guangzhou, China, pp. 144-153. (CCF C)
  40. 赵永望等. “形式化方法的研究进展与趋势”. 中国计算机学会CCF 2017-2018中国计算机科学技术发展报告, 1-68, 2018. 机械工业出版社.
  41. 赵永望, 冯新宇, "防黑客编程", 中国计算机学会通讯, 第13卷, 第10期, 2017年10月 (译文).
  42. Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu, "Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement", IEEE Transactions on Industrial Informatics, Volume 12, No. 4, August, 2016, pp. 1321 - 1331. (影响因子 8.785) [PDF download]
  43. Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu, "High-Assurance Separation Kernels: A Survey on Formal Methods", CoRR abs/1701.01535 (2017) [PDF download]
  44. 赵永望, 胡春明, "基于公式的软件调试", 中国计算机学会通讯, 第12卷, 第9期, 2016年9月 (译文).
  45. David Sanan, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey, "Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code", 20th International Conference on Engineering of Complex Computer Systems (ICECCS 2015), December 9-12, Gold Coast, Australia (CCF C) .
  46. Kun Cheng, Yuebin Bai, Yongwang Zhao#, Yao Ma, Duo Lu, Yuanfeng Peng, Minxuan Zhou, " HV2M: A novel approach to boost inter-VM network performance for Xen-based HVMs ", Journal of Systems and Software, Volume 114, April 2016, pp.54–68. (CCF B)
  47. Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali,Kai Hu, Yongwang Zhao, Dianfu Ma, "Towards a Verified Compiler Prototype for the Synchronous Language SIGNAL", Frontiers of Computer Science, Volume 10, Issue 1 (February 2016), pp 37–53, Springer (CCF B) .
  48. 杨志斌,赵永望,黄志球, 胡凯,马殿富,Jean-Paul BODEVEIX, Mamoun FILALI, "基于同步语言的的时间可预测多线程代码生成方法", 软件学报, 2016, 27(3): 611-632.
  49. 杨志斌,胡凯,赵永望,马殿富,Jean-Paul BODEVEIX,"基于时间抽象状态机的AADL模型验证", 软件学报, 2015, 26(2): 202-222.
  50. Yongwang Zhao, Zhuqing Li, Hualei Shen, Dianfu Ma, "Development of Global Specification for Dynamically Adaptive Software", Computing, Volume 95, Issue 9 (2013), pp. 785-816, Springer (SCI-Indexed) [PDF download].
  51. Jing Li, Yongwang Zhao, Hailong Sun, Zibin Zheng, Dianfu Ma, "DH4SS: A Distributed Heuristic for QoS-Based Service Selection", International Journal of Web and Grid Services (IJWGS), Vol.7, No.4, 2011, pp.388-409 (Top journal in web services, SCI-Indexed)
  52. Hualei Shen, Dianfu Ma, Yongwang Zhao#, Hailong Sun, Sujun Sun, Rongwei Ye, Lei Huang, Bo Lang, Yan Sun, "MIAPS: a web-based system for remotely accessing and presenting medical images", Computer Methods and Programs in Biomedicine, Volume 113, Issue 1 (January, 2014), pp. 266–283, Elsevier(SCI-Indexed).
  53. Yongwang Zhao, Chunyang Hu, Hualei Shen, Dianfu Ma, Xuan Li, Yonggang Huang, "A Hierarchical Organization Approach of Multi-dimensional Remote Sensing Data for Lightweight Web Map Services", Earth Science Informatics, Volume 5, Issue 1 (2012), pp. 61-75, Springer (SCI-Indexed).
  54. Hao, Zeng, Dianfu Ma, Yongwang Zhao, Zhuqing Li, "PBA4WSSP: A Policy-Based Architecture for Web Services Security Processing", Service Oriented Computing and Applications, Volume 8, Issue 1 (March, 2014), pp. 55 - 72, Springer (CCF C).
  55. Bingyang Zhao, Yongwang Zhao, Dianfu Ma, "A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems", 15th IEEE symposium on object/component/service-oriented realtime distributed computing(ISORC 2012), IEEE Computer Society, April 11-13, 2012, Shenzhen, China, pp.103-110.
  56. Ying Wang, Dianfu Ma, Yongwang Zhao, Lu Zou, Xianqi Zhao, "Automatic RT-Java code generation from AADL models for ARINC653-based avionics software", 36th IEEE Computer Software and Applications Conference (COMPSAC 2012), IEEE Computer Society, July 16-20, 2012, Izmir, Turkey (CCF B) .
  57. Ying Wang, Dianfu Ma, Yongwang Zhao, "An AADL-based modeling method for ARINC653-based avionics software", 35th IEEE Computer Software and Applications Conference (COMPSAC 2011) , IEEE Computer Society, July 18-22, 2011, Munich, German, pp.224-229 (CCF B) .
  58. Zhuqing Li, Dianfu Ma, Yongwang Zhao, Jing Li, Qing Yang, "FSM4WSR: A Formal Model for Verifiable Web Service Runtime", Proceedings of 2011 IEEE Asia-Pacific Services Computing Conference (APSCC 2011), IEEE Computer Society, December 12 - 15, 2011, Jeju, Korea, pp.86-93.