| 2026 | TASE | Formal Verification of a Rust-Based Buddy Physical Memory Allocator. | Shaojie Wang, Yuting Wang, Qianying Zhang, Weituo Dai, Tian'ao Xie, Shijun Zhao, Yongwang Zhao |
| 2025 | CCS | Generalized Security-Preserving Refinement for Concurrent Systems. | Huan Sun, David Sann, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang |
| 2024 | SETTA | Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. | Jiayi Lu, Shenghao Yuan, David Sann, Yongwang Zhao |
| 2024 | TACAS | A Comprehensive Specification and Verification of the L4 Microkernel API. | Leping Zhang, Yongwang Zhao, Jianxin Li |
| 2023 | ICWS | VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks. | Zhuoruo Zhang, Jilin Hu, Chenyang Yu, Rui Chang, Yongwang Zhao |
| 2023 | ISSRE | Lark: Verified Cross-Domain Access Control for Trusted Execution Environments. | Fanlang Zeng, Zhuoruo Zhang, Rui Chang, Chenyang Yu, Zijun Zhang, Yongwang Zhao |
| 2022 | ICFEM | A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. | Ke Jiang, Tianwei Zhang, David Sann, Yongwang Zhao, Yang Liu |
| 2021 | FM | Apply Formal Methods in Certifying the SyberX High-Assurance Kernel. | Wenjing Xu, Yongwang Zhao, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang, Shihong Zou |
| 2020 | TASE | Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles. | Wenjing Xul, Yongwang Zhao, Dianfu Ma, YuXin Zhang, Qian Xiao |
| 2019 | CAV | Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. | Yongwang Zhao, David Sann |
| 2019 | FM | A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. | Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu |
| 2019 | ICECCS | A Formally Verified Buddy Memory Allocation Model. | Ke Jiang, David Sann, Yongwang Zhao, Shuanglong Kan, Yang Liu |
| 2019 | ISORC | Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS. | Feng Zhang, Yongwang Zhao, Dianfu Ma, Wensheng Niu |
| 2019 | SETTA | A Verified Specification of TLSF Memory Management Allocator Using State Monads. | Yu Zhang, Yongwang Zhao, David Sann, Lei Qiao, Jinkun Zhang |
| 2018 | FM | Compositional Reasoning for Shared-Variable Concurrent Programs. | Fuyuan Zhang, Yongwang Zhao, David Sann, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun |
| 2017 | TACAS | CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. | David Sann, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu |
| 2016 | TACAS | Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. | Yongwang Zhao, David Sann, Fuyuan Zhang, Yang Liu |
| 2015 | ICECCS | Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. | David Sann, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey |
| 2015 | ISSRE | Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. | Yongwang Zhao, Zhibin Yang, David Sann, Yang Liu |
| 2014 | KSEM | Formal Modeling of Airborne Software High-Level Requirements Based on Knowledge Graph. | Wenjuan Wu, Dianfu Ma, Yongwang Zhao, Xianqi Zhao |
| 2013 | DASC | A Web Services Container Supporting QoS Hierarchical Control with Multiple Measurements for Utilization. | Zhe Wang, Dianfu Ma, Yongwang Zhao |
| 2013 | ISCC | A policy-based architecture for web services authentication. | Hao Zeng, Dianfu Ma, Yongwang Zhao, Zhuqing Li |
| 2012 | COMPSAC | Automatic RT-Java Code Generation from AADL Models for ARINC653-Based Avionics Software. | Ying Wang, Dianfu Ma, Yongwang Zhao, Lu Zou, Xianqi Zhao |
| 2012 | ISORC | A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems. | Bingyang Zhao, Yongwang Zhao, Dianfu Ma |
| 2011 | AINA | Geospatial Web Service for Remote Sensing Data Visualization. | Chunyang Hu, Yongwang Zhao, Jing Li, Dianfu Ma, Xuan Li |
| 2011 | AINA | Towards Verifying Global Properties of Adaptive Software Based on Linear Temporal Logic. | Yongwang Zhao, Jing Li, Dou Sun, Dianfu Ma |
| 2011 | APSCC | FSM4WSR: A Formal Model for Verifiable Web Service Runtime. | Zhuqing Li, Dianfu Ma, Yongwang Zhao, Jing Li, Qing Yang |
| 2011 | APSCC | Integrating Business Processes and Business Rules. | Yujing Zhao, Dianfu Ma, Yongwang Zhao, Zhuqing Li |
| 2011 | COMPSAC | An AADL-Based Modeling Method for ARINC653-Based Avionics Software. | Ying Wang, Dianfu Ma, Yongwang Zhao, Lu Zou, Xianqi Zhao |
| 2010 | APSCC | Towards a Formal Verification Approach for Implementation of Web Services Specifications. | Qing Yang, Dianfu Ma, Yongwang Zhao, Zhuqing Li |
| 2010 | IIWAS | OGC-compatible high-performance web map service for remote sensing data visualization. | Chunyang Hu, Yongwang Zhao, Jing Li, Min Liu, Dianfu Ma, Xuan Li |
| 2010 | ISCC | ACTGIS: A Web-based collaborative tiled Geospatial image map system. | Chunyang Hu, Yongwang Zhao, Xin Wei, Bowen Du, Yonggang Huang, Dianfu Ma, Xuan Li |
| 2010 | ISCC | An adaptive heuristic approach for distributed QoS-based service composition. | Jing Li, Yongwang Zhao, Min Liu, Hailong Sun, Dianfu Ma |
| 2010 | ISCC | SEDA4BPEL: A staged event-driven architecture for high-concurrency BPEL engine. | Dou Sun, Yongwang Zhao, Hao Zeng, Dianfu Ma |
| 2010 | UIC | Formal Analysis of Behavioural Equivalence for Trustworthy and Composite Web Services. | Yongwang Zhao, Chunyang Hu, Min Liu, Dianfu Ma |
| 2009 | ICIW | An Approach to Preserving Consistency of SOAs in Dynamic Evolution. | Min Liu, Dianfu Ma, Yongwang Zhao, Dou Sun |
| 2009 | PDP | A Graph Transformation based Approach for Runtime Constrained Evolution of Service-Oriented Architectures. | Yongwang Zhao, Dianfu Ma, Min Liu, Chunyang Hu, Yongwang Huang |
| 2009 | SAC | An approach to identifying conversation dependency in service oriented system during dynamic evolution. | Min Liu, Dianfu Ma, Yongwang Zhao |
| 2008 | PRDC | Reliability Quantification of the Tree Structure Based Distributed System. | Dianfu Ma, Min Liu, Yongwang Zhao, Dou Sun |
| 2008 | SAC | SSCM: middleware for structure-based service collaboration. | Dianfu Ma, Min Liu, Yongwang Zhao, Chunyang Hu |
| 2007 | ICIW | Collaborative Visualization of Large Scale Datasets Using Web Services. | Yongwang Zhao, Chunyang Hu, Yonggang Huang, Dianfu Ma |
| 2007 | ISPDC | SOCOM: A Service-Oriented Collaboration Middleware for Multi-User Interaction with Web Services based Scientific Resources. | Yongwang Zhao, Dianfu Ma, Chunyang Hu, Min Liu, Yonggang Huang |