Yongwang Zhao - RankMe

106 papers A* 1A 4B 9C 19Misc 5Journal 49Unranked 19

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	K-SELinux: formal analysis and verification of SELinux policies via semantic execution. Frontiers Comput. Sci. Jinhui Kang, Jianhong Zhao, Yongwang Zhao
2026	J	`jnl`	PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot Under Hardware Supply-Chain Attacks. IEEE Trans. Inf. Forensics Secur. Zhuoruo Zhang, Rui Chang, Mingshuai Chen, Wenbo Shen, Chenyang Yu, He Huang, Qinming Dai, Yongwang Zhao
2026	J	`jnl`	Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4. CoRR Jianyu Zhang, Fuyuan Zhang, Jiayi Lu, Jilin Hu, Xiaoyi Yin, Long Zhang, Feng Yang, Yongwang Zhao
2025	J	`jnl`	A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana. Proc. ACM Program. Lang. Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanán, Rui Chang, Yongwang Zhao
2025	J	`jnl`	A Comprehensive Formal Specification of ARINC 653 With Conformity Proof. Softw. Test. Verification Reliab. Zhang Feng, Yongwang Zhao, Liu Yang, Jun Sun
2025	J	`jnl`	Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics. CoRR Jianhong Zhao, Everett Hildenbrandt, Juan Conejero, Yongwang Zhao
2025	A*	`conf`	Generalized Security-Preserving Refinement for Concurrent Systems. CCS Huan Sun, David Sanán, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang
2025	J	`jnl`	Generalized Security-Preserving Refinement for Concurrent Systems. CoRR Huan Sun, David Sanán, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang
2025	J	`jnl`	HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement. CoRR Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer
2025	J	`jnl`	KBX: Verified Model Synchronization via Formal Bidirectional Transformation. ACM Trans. Softw. Eng. Methodol. Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, Kui Ren
2025	J	`jnl`	Psychometric-Based Evaluation for Theorem Proving with Large Language Models. CoRR Jianyu Zhang, Yongwang Zhao, Long Zhang, Jilin Hu, Xiaokun Luan, Zhiwei Xu, Feng Yang
2025	J	`jnl`	Tacco: A Framework for Ensuring the Security of Real-World TEEs via Formal Verification. IEEE Trans. Dependable Secur. Comput. Jilin Hu, Yongwang Zhao, Shuangquan Pan, Zuohua Ding, Kui Ren
2024	—	`conf`	A Comprehensive Specification and Verification of the L4 Microkernel API. TACAS (2) Leping Zhang, Yongwang Zhao, Jianxin Li
2024	Misc	`conf`	Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. SETTA Jiayi Lu, Shenghao Yuan, David Sanán, Yongwang Zhao
2024	J	`jnl`	K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs. CoRR Jianhong Zhao, Jinhui Kang, Yongwang Zhao
2024	J	`jnl`	KBX: Verified Model Synchronization via Formal Bidirectional Transformation. CoRR Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, Kui Ren
2024	J	`jnl`	ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile. IEEE Trans. Dependable Secur. Comput. Jilin Hu, Fanlang Zeng, Yongwang Zhao, Zhuoruo Zhang, Leping Zhang, Jianhong Zhao, Rui Chang, Kui Ren
2023	J	`jnl`	CVTEE: A Compatible Verified TEE Architecture With Enhanced Security. IEEE Trans. Dependable Secur. Comput. Xinliang Miao, Rui Chang, Jianhong Zhao, Yongwang Zhao, Shuang Cao, Tao Wei, Liehui Jiang, Kui Ren
2023	J	`jnl`	Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems. CoRR Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2023	—	`conf`	Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving. Internetware Hao Xu, Yongwang Zhao
2023	A	`conf`	Lark: Verified Cross-Domain Access Control for Trusted Execution Environments. ISSRE Fanlang Zeng, Zhuoruo Zhang, Rui Chang, Chenyang Yu, Zijun Zhang, Yongwang Zhao
2023	J	`jnl`	Preface to the Special Issue on Constraint Solving and Theorem Proving. Int. J. Softw. Informatics Shaowei Cai, Zhenbang Chen, Ji Wang, Bohua Zhan, Yongwang Zhao
2023	J	`jnl`	Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone. Int. J. Softw. Informatics Fanlang Zeng, Rui Chang, Hao Xu, Shaoping Pan, Yongwang Zhao
2023	J	`jnl`	Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B. Formal Aspects Comput. Feng Zhang, Leping Zhang, Yongwang Zhao, Yang Liu, Jun Sun
2023	J	`jnl`	Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security. CoRR Yongwang Zhao, David Sanán
2023	J	`jnl`	Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications. CoRR Yongwang Zhao, David Sanán
2023	A	`conf`	VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks. ICWS Zhuoruo Zhang, Jilin Hu, Chenyang Yu, Rui Chang, Yongwang Zhao
2022	J	`jnl`	A Comprehensive Formalization of AADL with Behavior Annex. Sci. Program. Yu Tan, Yongwang Zhao, Dianfu Ma, Xuejun Zhang
2022	C	`conf`	A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. ICFEM Ke Jiang, Tianwei Zhang, David Sanán, Yongwang Zhao, Yang Liu
2022	—	`conf`	Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE. Internetware Xinliang Miao, Fanlang Zeng, Rui Chang, Chenyang Yu, Zijun Zhang, Liehui Jiang, Yongwang Zhao
2022	J	`jnl`	PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot. CoRR Zhuoruo Zhang, Chenyang Yu, He Huang, Rui Chang, Mingshuai Chen, Qinming Dai, Wenbo Shen, Yongwang Zhao, Kui Ren
2021	J	`jnl`	Accelerator Virtualization Framework Based on Inter-VM Exitless Communication. Int. J. Softw. Informatics Dingji Li, Zeyu Mi, Baodong Wu, Xun Chen, Yongwang Zhao, Zuohua Ding, Haibo Chen
2021	B	`conf`	Apply Formal Methods in Certifying the SyberX High-Assurance Kernel. FM Wenjing Xu, Yongwang Zhao, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang, Shihong Zou
2021	J	`jnl`	CSim ACM Trans. Program. Lang. Syst. David Sanán, Yongwang Zhao, Shang-Wei Lin, Yang Liu
2021	J	`jnl`	Model learning: a survey of foundations, tools and applications. Frontiers Comput. Sci. Shahbaz Ali, Hailong Sun, Yongwang Zhao
2020	Misc	`conf`	Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles. TASE Wenjing Xul, Yongwang Zhao, Dianfu Ma, Yuxin Zhang, Qian Xiao
2019	B	`conf`	A Formally Verified Buddy Memory Allocation Model. ICECCS Ke Jiang, David Sanán, Yongwang Zhao, Shuanglong Kan, Yang Liu
2019	B	`conf`	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. FM Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2019	Misc	`conf`	A Verified Specification of TLSF Memory Management Allocator Using State Monads. SETTA Yu Zhang, Yongwang Zhao, David Sanán, Lei Qiao, Jinkun Zhang
2019	—	`conf`	Combining Model Learning and Model Checking to Analyze Java Libraries. SOFL+MSVL Shahbaz Ali, Hailong Sun, Yongwang Zhao
2019	C	`conf`	Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS. ISORC Feng Zhang, Yongwang Zhao, Dianfu Ma, Wensheng Niu
2019	J	`jnl`	Model Learning: A Survey on Foundation, Tools and Applications. CoRR Shahbaz Ali, Hailong Sun, Yongwang Zhao
2019	J	`jnl`	Refinement-Based Specification and Security Analysis of Separation Kernels. IEEE Trans. Dependable Secur. Comput. Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2019	—	`conf`	Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. CAV (2) Yongwang Zhao, David Sanán
2018	J	`jnl`	A Verified Capability-Based Model for Information Flow Security With Dynamic Policies. IEEE Access Jianwen Sun, Xiang Long, Yongwang Zhao
2018	J	`jnl`	A Verified Timsort C Implementation in Isabelle/HOL. CoRR Yu Zhang, Yongwang Zhao, David Sanán
2018	J	`jnl`	An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems. CoRR Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2018	B	`conf`	Compositional Reasoning for Shared-Variable Concurrent Programs. FM Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun
2017	J	`jnl`	A survey on formal specification and verification of separation kernels. Frontiers Comput. Sci. Yongwang Zhao, Zhibin Yang, Dianfu Ma
2017	—	`conf`	CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. TACAS (1) David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu
2017	J	`jnl`	Formal Verification of Behavioral AADL Models by Stateful Timed CSP. IEEE Access Feng Zhang, Yongwang Zhao, Dianfu Ma, Wensheng Niu
2017	J	`jnl`	High-Assurance Separation Kernels: A Survey on Formal Methods. CoRR Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2017	J	`jnl`	Refinement-based Specification and Security Analysis of Separation Kernels. CoRR Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2016	J	`jnl`	Compositional Reasoning for Shared-variable Concurrent Programs. CoRR Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Zhimin Wu, Jun Sun
2016	J	`jnl`	Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement. IEEE Trans. Ind. Informatics Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2016	J	`jnl`	HV J. Syst. Softw. Kun Cheng, Yuebin Bai, Yongwang Zhao, Yao Ma, Duo Lu, Yuanfeng Peng, Minxuan Zhou
2016	A	`conf`	Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. TACAS Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2016	J	`jnl`	Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers Comput. Sci. Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu, Yongwang Zhao, Dianfu Ma
2015	J	`jnl`	Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B. CoRR Yongwang Zhao, Zhibin Yang, David Sanán
2015	A	`conf`	Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B. ISSRE Yongwang Zhao, Zhibin Yang, David Sanán, Yang Liu
2015	J	`jnl`	Formal Specification and Verification of Separation Kernels: An Overview. CoRR Yongwang Zhao
2015	J	`jnl`	Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication. CoRR Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
2015	B	`conf`	Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code. ICECCS David Sanán, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey
2014	C	`conf`	Formal Modeling of Airborne Software High-Level Requirements Based on Knowledge Graph. KSEM Wenjuan Wu, Dianfu Ma, Yongwang Zhao, Xianqi Zhao
2014	J	`jnl`	MIAPS: A web-based system for remotely accessing and presenting medical images. Comput. Methods Programs Biomed. Hualei Shen, Dianfu Ma, Yongwang Zhao, Hailong Sun, Sujun Sun, Rongwei Ye, Lei Huang, Bo Lang, Yan Sun
2014	J	`jnl`	PBA4WSSP: a policy-based architecture for web services security processing. Serv. Oriented Comput. Appl. Hao Zeng, Dianfu Ma, Yongwang Zhao, Zhuqing Li
2014	—	`conf`	Query dependent multiview features fusion for effective medical image retrieval. SPAC Hualei Shen, Yongwang Zhao, Dianfu Ma, Yong Guan
2013	C	`conf`	A Web Services Container Supporting QoS Hierarchical Control with Multiple Measurements for Utilization. DASC Zhe Wang, Dianfu Ma, Yongwang Zhao
2013	C	`conf`	A policy-based architecture for web services authentication. ISCC Hao Zeng, Dianfu Ma, Yongwang Zhao, Zhuqing Li
2013	J	`jnl`	Development of global specification for dynamically adaptive software. Computing Yongwang Zhao, Zhuqing Li, Hualei Shen, Dianfu Ma
2012	C	`conf`	A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems. ISORC Bingyang Zhao, Yongwang Zhao, Dianfu Ma
2012	J	`jnl`	A New Re-Ranking Method Using Enhanced Pseudo-Relevance Feedback for Content-Based Medical Image Retrieval. IEICE Trans. Inf. Syst. Yonggang Huang, Jun Zhang, Yongwang Zhao, Dianfu Ma
2012	—	`conf`	A Policy-Based Architecture for Web Services Security Processing. ICEBE Hao Zeng, Dianfu Ma, Zhuqing Li, Yongwang Zhao
2012	J	`jnl`	A hierarchical organization approach of multi-dimensional remote sensing data for lightweight Web Map Services. Earth Sci. Informatics Yongwang Zhao, Chunyang Hu, Hualei Shen, Dianfu Ma, Xuan Li, Yonggang Huang
2012	B	`conf`	Automatic RT-Java Code Generation from AADL Models for ARINC653-Based Avionics Software. COMPSAC Ying Wang, Dianfu Ma, Yongwang Zhao, Lu Zou, Xianqi Zhao
2012	—	`conf`	Collaborative annotation of medical images via web browser for teleradiology. ICCH Hualei Shen, Dianfu Ma, Yongwang Zhao, Rongwei Ye
2012	—	`conf`	Managing and Collaboratively Processing Medical Image via the Web. WAIM Workshops Hualei Shen, Dianfu Ma, Yongwang Zhao, Chunyao Yang, Sujun Sun, Bo Lang
2012	J	`jnl`	QDFA: Query-Dependent Feature Aggregation for Medical Image Retrieval. IEICE Trans. Inf. Syst. Yonggang Huang, Dianfu Ma, Jun Zhang, Yongwang Zhao
2011	B	`conf`	An AADL-Based Modeling Method for ARINC653-Based Avionics Software. COMPSAC Ying Wang, Dianfu Ma, Yongwang Zhao, Lu Zou, Xianqi Zhao
2011	—	`conf`	Building high-speed roads: Improving performance of SOAP processing for cloud services. SOSE Huang Liu, Xudong Liu, Jianxin Li, Yongwang Zhao, Zhuqing Li
2011	J	`jnl`	DH4SS: a distributed heuristic for QoS-based service selection. Int. J. Web Grid Serv. Jing Li, Yongwang Zhao, Hailong Sun, Zibin Zheng, Dianfu Ma
2011	C	`conf`	FSM4WSR: A Formal Model for Verifiable Web Service Runtime. APSCC Zhuqing Li, Dianfu Ma, Yongwang Zhao, Jing Li, Qing Yang
2011	B	`conf`	Geospatial Web Service for Remote Sensing Data Visualization. AINA Chunyang Hu, Yongwang Zhao, Jing Li, Dianfu Ma, Xuan Li
2011	C	`conf`	Integrating Business Processes and Business Rules. APSCC Yujing Zhao, Dianfu Ma, Yongwang Zhao, Zhuqing Li
2011	C	`conf`	SCENETester: A Testing Framework to Support Fault Diagnosis for Web Service Composition. CIT Zekun Zhu, Jianxin Li, Yongwang Zhao, Zhuqing Li
2011	—	`conf`	Towards Hierarchical Modeling and Analysis of Web Services Choreography. IESS Yongwang Zhao, Jing Li, Zhuqing Li, Dianfu Ma
2011	B	`conf`	Towards Verifying Global Properties of Adaptive Software Based on Linear Temporal Logic. AINA Yongwang Zhao, Jing Li, Dou Sun, Dianfu Ma
2010	C	`conf`	ACTGIS: A Web-based collaborative tiled Geospatial image map system. ISCC Chunyang Hu, Yongwang Zhao, Xin Wei, Bowen Du, Yonggang Huang, Dianfu Ma, Xuan Li
2010	C	`conf`	An adaptive heuristic approach for distributed QoS-based service composition. ISCC Jing Li, Yongwang Zhao, Min Liu, Hailong Sun, Dianfu Ma
2010	—	`conf`	An operational semantics of WS-BPEL based on abstract BPEL machine. SOCA Dou Sun, Yongwang Zhao, Hao Zeng, Dianfu Ma
2010	—	`conf`	Formal Analysis of Behavioural Equivalence for Trustworthy and Composite Web Services. UIC/ATC Workshops Yongwang Zhao, Chunyang Hu, Min Liu, Dianfu Ma
2010	—	`conf`	Medical Image Retrieval with Query-Dependent Feature Fusion Based on One-Class SVM. CSE Yonggang Huang, Jun Zhang, Yongwang Zhao, Dianfu Ma
2010	C	`conf`	OGC-compatible high-performance web map service for remote sensing data visualization. iiWAS Chunyang Hu, Yongwang Zhao, Jing Li, Min Liu, Dianfu Ma, Xuan Li
2010	C	`conf`	SEDA4BPEL: A staged event-driven architecture for high-concurrency BPEL engine. ISCC Dou Sun, Yongwang Zhao, Hao Zeng, Dianfu Ma
2010	C	`conf`	Towards a Formal Verification Approach for Implementation of Web Services Specifications. APSCC Qing Yang, Dianfu Ma, Yongwang Zhao, Zhuqing Li
2010	—	`conf`	Towards a Graph Grammar Based Verification Approach for Runtime Constrained Evolution of Service-Oriented Architectures. SOSE Yongwang Zhao, Bingyang Zhao, Min Liu, Chunyang Hu, Dianfu Ma
2010	—	`conf`	Towards adaptive web services QoS prediction. SOCA Jing Li, Yongwang Zhao, Jiawen Ren, Dianfu Ma
2009	C	`conf`	A Graph Transformation based Approach for Runtime Constrained Evolution of Service-Oriented Architectures. PDP Yongwang Zhao, Dianfu Ma, Min Liu, Chunyang Hu, Yongwang Huang
2009	C	`conf`	An Approach to Preserving Consistency of SOAs in Dynamic Evolution. ICIW Min Liu, Dianfu Ma, Yongwang Zhao, Dou Sun
2009	Misc	`conf`	An approach to identifying conversation dependency in service oriented system during dynamic evolution. SAC Min Liu, Dianfu Ma, Yongwang Zhao
2008	—	`conf`	Collaborative geospatial web services for multi-dimension remote sensing data. ICDIM Chunyang Hu, Yongwang Zhao, Dianfu Ma, Xiaoliang Sun, Jun Shao, Xuan Li
2008	—	`conf`	Coordination Behavioral Structure: A Web Services Coordination Model in Dynamic Environment. ACIS-ICIS Yongwang Zhao, Dianfu Ma, Min Liu, Chunyang Hu
2008	C	`conf`	Reliability Quantification of the Tree Structure Based Distributed System. PRDC Dianfu Ma, Min Liu, Yongwang Zhao, Dou Sun
2008	Misc	`conf`	SSCM: middleware for structure-based service collaboration. SAC Dianfu Ma, Min Liu, Yongwang Zhao, Chunyang Hu
2007	C	`conf`	Collaborative Visualization of Large Scale Datasets Using Web Services. ICIW Yongwang Zhao, Chunyang Hu, Yonggang Huang, Dianfu Ma
2007	C	`conf`	SOCOM: A Service-Oriented Collaboration Middleware for Multi-User Interaction with Web Services based Scientific Resources. ISPDC Yongwang Zhao, Dianfu Ma, Chunyang Hu, Min Liu, Yonggang Huang