Collaborative Visualization of Large Scale Datasets Using Web Services. - Yongwang Zhao; Chunyang Hu; Yonggang Huang; Dianfu Ma (ICIW, 2007)

SOCOM: A Service-Oriented Collaboration Middleware for Multi-User Interaction with Web Services based Scientific Resources. - Yongwang Zhao; Dianfu Ma; Chunyang Hu; Min Liu 017; Yonggang Huang (ISPDC, 2007)

Coordination Behavioral Structure: A Web Services Coordination Model in Dynamic Environment. - Yongwang Zhao; Dianfu Ma; Min Liu 017; Chunyang Hu (ACIS-ICIS, 2008)

Collaborative geospatial web services for multi-dimension remote sensing data. - Chunyang Hu; Yongwang Zhao; Dianfu Ma; Xiaoliang Sun; Jun Shao; Xuan Li (ICDIM, 2008)

Reliability Quantification of the Tree Structure Based Distributed System. - Dianfu Ma; Min Liu 017; Yongwang Zhao; Dou Sun (PRDC, 2008)

SSCM: middleware for structure-based service collaboration. - Dianfu Ma; Min Liu 017; Yongwang Zhao; Chunyang Hu (SAC, 2008)

An Approach to Preserving Consistency of SOAs in Dynamic Evolution. - Min Liu 017; Dianfu Ma; Yongwang Zhao; Dou Sun (ICIW, 2009)

A Graph Transformation based Approach for Runtime Constrained Evolution of Service-Oriented Architectures. - Yongwang Zhao; Dianfu Ma; Min Liu 017; Chunyang Hu; Yongwang Huang (PDP, 2009)

An approach to identifying conversation dependency in service oriented system during dynamic evolution. - Min Liu 017; Dianfu Ma; Yongwang Zhao (SAC, 2009)

Towards a Formal Verification Approach for Implementation of Web Services Specifications. - Qing Yang; Dianfu Ma; Yongwang Zhao; Zhuqing Li (APSCC, 2010)

Medical Image Retrieval with Query-Dependent Feature Fusion Based on One-Class SVM. - Yonggang Huang; Jun Zhang 010; Yongwang Zhao; Dianfu Ma (CSE, 2010)

OGC-compatible high-performance web map service for remote sensing data visualization. - Chunyang Hu; Yongwang Zhao; Jing Li 075; Min Liu 017; Dianfu Ma; Xuan Li (iiWAS, 2010)

ACTGIS: A Web-based collaborative tiled Geospatial image map system. - Chunyang Hu; Yongwang Zhao; Xin Wei; Bowen Du; Yonggang Huang; Dianfu Ma; Xuan Li (ISCC, 2010)

An adaptive heuristic approach for distributed QoS-based service composition. - Jing Li 075; Yongwang Zhao; Min Liu 017; Hailong Sun 001; Dianfu Ma (ISCC, 2010)

SEDA4BPEL: A staged event-driven architecture for high-concurrency BPEL engine. - Dou Sun; Yongwang Zhao; Hao Zeng; Dianfu Ma (ISCC, 2010)

Towards adaptive web services QoS prediction. - Jing Li 075; Yongwang Zhao; Jiawen Ren; Dianfu Ma (SOCA, 2010)

An operational semantics of WS-BPEL based on abstract BPEL machine. - Dou Sun; Yongwang Zhao; Hao Zeng; Dianfu Ma (SOCA, 2010)

Towards a Graph Grammar Based Verification Approach for Runtime Constrained Evolution of Service-Oriented Architectures. - Yongwang Zhao; Bingyang Zhao; Min Liu 017; Chunyang Hu; Dianfu Ma (SOSE, 2010)

Formal Analysis of Behavioural Equivalence for Trustworthy and Composite Web Services. - Yongwang Zhao; Chunyang Hu; Min Liu 017; Dianfu Ma (UIC/ATC Workshops, 2010)

SCENETester: A Testing Framework to Support Fault Diagnosis for Web Service Composition. - Zekun Zhu; Jianxin Li 002; Yongwang Zhao; Zhuqing Li (CIT, 2011)

Geospatial Web Service for Remote Sensing Data Visualization. - Chunyang Hu; Yongwang Zhao; Jing Li 075; Dianfu Ma; Xuan Li (AINA, 2011)

Towards Verifying Global Properties of Adaptive Software Based on Linear Temporal Logic. - Yongwang Zhao; Jing Li 075; Dou Sun; Dianfu Ma (AINA, 2011)

FSM4WSR: A Formal Model for Verifiable Web Service Runtime. - Zhuqing Li; Dianfu Ma; Yongwang Zhao; Jing Li 075; Qing Yang (APSCC, 2011)

Integrating Business Processes and Business Rules. - Yujing Zhao; Dianfu Ma; Yongwang Zhao; Zhuqing Li (APSCC, 2011)

An AADL-Based Modeling Method for ARINC653-Based Avionics Software. - Ying Wang; Dianfu Ma; Yongwang Zhao; Lu Zou; Xianqi Zhao (COMPSAC, 2011)

Towards Hierarchical Modeling and Analysis of Web Services Choreography. - Yongwang Zhao; Jing Li 075; Zhuqing Li; Dianfu Ma (IESS, 2011)

Building high-speed roads: Improving performance of SOAP processing for cloud services. - Huang Liu; Xudong Liu 001; Jianxin Li 002; Yongwang Zhao; Zhuqing Li (SOSE, 2011)

DH4SS: a distributed heuristic for QoS-based service selection. - Jing Li 075; Yongwang Zhao; Hailong Sun 001; Zibin Zheng; Dianfu Ma (Int. J. Web Grid Serv., 2011)

Automatic RT-Java Code Generation from AADL Models for ARINC653-Based Avionics Software. - Ying Wang; Dianfu Ma; Yongwang Zhao; Lu Zou; Xianqi Zhao (COMPSAC, 2012)

Collaborative annotation of medical images via web browser for teleradiology. - Hualei Shen; Dianfu Ma; Yongwang Zhao; Rongwei Ye (ICCH, 2012)

A Policy-Based Architecture for Web Services Security Processing. - Hao Zeng; Dianfu Ma; Zhuqing Li; Yongwang Zhao (ICEBE, 2012)

A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems. - Bingyang Zhao; Yongwang Zhao; Dianfu Ma (ISORC, 2012)

Managing and Collaboratively Processing Medical Image via the Web. - Hualei Shen; Dianfu Ma; Yongwang Zhao; Chunyao Yang; Sujun Sun; Bo Lang (WAIM Workshops, 2012)

A hierarchical organization approach of multi-dimensional remote sensing data for lightweight Web Map Services. - Yongwang Zhao; Chunyang Hu; Hualei Shen; Dianfu Ma; Xuan Li; Yonggang Huang (Earth Sci. Informatics, 2012)

QDFA: Query-Dependent Feature Aggregation for Medical Image Retrieval. - Yonggang Huang; Dianfu Ma; Jun Zhang 010; Yongwang Zhao (IEICE Trans. Inf. Syst., 2012)

A New Re-Ranking Method Using Enhanced Pseudo-Relevance Feedback for Content-Based Medical Image Retrieval. - Yonggang Huang; Jun Zhang 010; Yongwang Zhao; Dianfu Ma (IEICE Trans. Inf. Syst., 2012)

A Web Services Container Supporting QoS Hierarchical Control with Multiple Measurements for Utilization. - Zhe Wang 024; Dianfu Ma; Yongwang Zhao (DASC, 2013)

A policy-based architecture for web services authentication. - Hao Zeng; Dianfu Ma; Yongwang Zhao; Zhuqing Li (ISCC, 2013)

Development of global specification for dynamically adaptive software. - Yongwang Zhao; Zhuqing Li; Hualei Shen; Dianfu Ma (Computing, 2013)

Formal Modeling of Airborne Software High-Level Requirements Based on Knowledge Graph. - Wenjuan Wu; Dianfu Ma; Yongwang Zhao; Xianqi Zhao (KSEM, 2014)

Query dependent multiview features fusion for effective medical image retrieval. - Hualei Shen; Yongwang Zhao; Dianfu Ma; Yong Guan (SPAC, 2014)

MIAPS: A web-based system for remotely accessing and presenting medical images. - Hualei Shen; Dianfu Ma; Yongwang Zhao; Hailong Sun 001; Sujun Sun; Rongwei Ye; Lei Huang 015; Bo Lang; Yan Sun (Comput. Methods Programs Biomed., 2014)

PBA4WSSP: a policy-based architecture for web services security processing. - Hao Zeng; Dianfu Ma; Yongwang Zhao; Zhuqing Li (Serv. Oriented Comput. Appl., 2014)

Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. - David Sanán; Yang Liu 003; Yongwang Zhao; Zhenchang Xing; Mike Hinchey (ICECCS, 2015)

Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. - Yongwang Zhao; Zhibin Yang; David Sanán; Yang Liu 003 (ISSRE, 2015)

Formal Specification and Verification of Separation Kernels: An Overview. - Yongwang Zhao (CoRR, 2015)

Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B. - Yongwang Zhao; Zhibin Yang; David Sanán (CoRR, 2015)

Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (TACAS, 2016)

Compositional Reasoning for Shared-variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Zhimin Wu; Jun Sun 001 (CoRR, 2016)

Towards a verified compiler prototype for the synchronous language SIGNAL. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Kai Hu 004; Yongwang Zhao; Dianfu Ma (Frontiers Comput. Sci., 2016)

HV2M: A novel approach to boost inter-VM network performance for Xen-based HVMs. - Kun Cheng; Yuebin Bai; Yongwang Zhao; Yao Ma; Duo Lu; Yuanfeng Peng; Minxuan Zhou (J. Syst. Softw., 2016)

Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (IEEE Trans. Ind. Informatics, 2016)

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. - David Sanán; Yongwang Zhao; Zhe Hou; Fuyuan Zhang; Alwen Tiu; Yang Liu 003 (TACAS (1), 2017)

Formal Verification of Behavioral AADL Models by Stateful Timed CSP. - Feng Zhang; Yongwang Zhao; Dianfu Ma; Wensheng Niu (IEEE Access, 2017)

High-Assurance Separation Kernels: A Survey on Formal Methods. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2017)

A survey on formal specification and verification of separation kernels. - Yongwang Zhao; Zhibin Yang; Dianfu Ma (Frontiers Comput. Sci., 2017)

Compositional Reasoning for Shared-Variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Jun Sun 001 (FM, 2018)

A Verified Capability-Based Model for Information Flow Security With Dynamic Policies. - Jianwen Sun; Xiang Long; Yongwang Zhao (IEEE Access, 2018)

An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2018)

A Verified Timsort C Implementation in Isabelle/HOL. - Yu Zhang; Yongwang Zhao; David Sanán (CoRR, 2018)

Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. - Yongwang Zhao; David Sanán (CAV (2), 2019)

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (FM, 2019)

A Formally Verified Buddy Memory Allocation Model. - Ke Jiang; David Sanán; Yongwang Zhao; Shuanglong Kan; Yang Liu 003 (ICECCS, 2019)

Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS. - Feng Zhang; Yongwang Zhao; Dianfu Ma; Wensheng Niu (ISORC, 2019)

A Verified Specification of TLSF Memory Management Allocator Using State Monads. - Yu Zhang; Yongwang Zhao; David Sanán; Lei Qiao; Jinkun Zhang (SETTA, 2019)

Combining Model Learning and Model Checking to Analyze Java Libraries. - Shahbaz Ali; Hailong Sun 001; Yongwang Zhao (SOFL+MSVL, 2019)

Model Learning: A Survey on Foundation, Tools and Applications. - Shahbaz Ali; Hailong Sun 001; Yongwang Zhao (CoRR, 2019)

Refinement-Based Specification and Security Analysis of Separation Kernels. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (IEEE Trans. Dependable Secur. Comput., 2019)

Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles. - Wenjing Xul; Yongwang Zhao; Dianfu Ma; YuXin Zhang; Qian Xiao (TASE, 2020)

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 (FM, 2021)

Model learning: a survey of foundations, tools and applications. - Shahbaz Ali; Hailong Sun 001; Yongwang Zhao (Frontiers Comput. Sci., 2021)

Accelerator Virtualization Framework Based on Inter-VM Exitless Communication. - Dingji Li; Zeyu Mi; Baodong Wu; Xun Chen; Yongwang Zhao; Zuohua Ding; Haibo Chen 001 (Int. J. Softw. Informatics, 2021)

CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee. - David Sanán; Yongwang Zhao; Shang-Wei Lin 001; Yang Liu 003 (ACM Trans. Program. Lang. Syst., 2021)

A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. - Ke Jiang; Tianwei Zhang 004; David Sanán; Yongwang Zhao; Yang Liu 003 (ICFEM, 2022)

Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE. - Xinliang Miao; Fanlang Zeng; Rui Chang; Chenyang Yu; Zijun Zhang; Liehui Jiang; Yongwang Zhao (Internetware, 2022)

PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot. - Zhuoruo Zhang; Chenyang Yu; He Huang; Rui Chang; Mingshuai Chen; Qinming Dai; Wenbo Shen; Yongwang Zhao; Kui Ren 001 (CoRR, 2022)

A Comprehensive Formalization of AADL with Behavior Annex. - Yu Tan; Yongwang Zhao; Dianfu Ma; Xuejun Zhang (Sci. Program., 2022)

VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks. - Zhuoruo Zhang; Jilin Hu; Chenyang Yu; Rui Chang; Yongwang Zhao (ICWS, 2023)

Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving. - Hao Xu; Yongwang Zhao (Internetware, 2023)

Lark: Verified Cross-Domain Access Control for Trusted Execution Environments. - Fanlang Zeng; Zhuoruo Zhang; Rui Chang; Chenyang Yu; Zijun Zhang; Yongwang Zhao (ISSRE, 2023)

Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems. - Yongwang Zhao; David Sanán; Fuyuan Zhang; Yang Liu 003 (CoRR, 2023)

Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications. - Yongwang Zhao; David Sanán (CoRR, 2023)

Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security. - Yongwang Zhao; David Sanán (CoRR, 2023)

Preface to the Special Issue on Constraint Solving and Theorem Proving. - Shaowei Cai 001; Zhenbang Chen; Ji Wang 001; Bohua Zhan; Yongwang Zhao (Int. J. Softw. Informatics, 2023)

Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone. - Fanlang Zeng; Rui Chang; Hao Xu; Shaoping Pan; Yongwang Zhao (Int. J. Softw. Informatics, 2023)

CVTEE: A Compatible Verified TEE Architecture With Enhanced Security. - Xinliang Miao; Rui Chang; Jianhong Zhao; Yongwang Zhao; Shuang Cao; Tao Wei 002; Liehui Jiang; Kui Ren 001 (IEEE Trans. Dependable Secur. Comput., 2023)

Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B. - Feng Zhang; Leping Zhang; Yongwang Zhao; Yang Liu 003; Jun Sun 001 (Formal Aspects Comput., 2023)

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 Comprehensive Specification and Verification of the L4 Microkernel API. - Leping Zhang; Yongwang Zhao; Jianxin Li 002 (TACAS (2), 2024)

K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs. - Jianhong Zhao; Jinhui Kang; Yongwang Zhao (CoRR, 2024)

ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile. - Jilin Hu; Fanlang Zeng; Yongwang Zhao; Zhuoruo Zhang; Leping Zhang; Jianhong Zhao; Rui Chang; Kui Ren 001 (IEEE Trans. Dependable Secur. Comput., 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)

A Comprehensive Formal Specification of ARINC 653 With Conformity Proof. - Zhang Feng; Yongwang Zhao; Liu Yang; Jun Sun 001 (Softw. Test. Verification Reliab., 2025)

Psychometric-Based Evaluation for Theorem Proving with Large Language Models. - Jianyu Zhang; Yongwang Zhao; Long Zhang; Jilin Hu; Xiaokun Luan; Zhiwei Xu; Feng Yang (CoRR, 2025)

KBX: Verified Model Synchronization via Formal Bidirectional Transformation. - Jianhong Zhao; Yongwang Zhao; Peisen Yao; Fanlang Zeng; Bohua Zhan; Kui Ren 001 (ACM Trans. Softw. Eng. Methodol., 2025)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement. - Jilin Hu; Jianyu Zhang; Yongwang Zhao; Talia Ringer (CoRR, 2025)