Yongwang Zhao

Jianxin Li

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023

Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B.

[BibT_eX]

[DOI]

Formal Aspects Comput., December, 2023

CVTEE: A Compatible Verified TEE Architecture With Enhanced Security.

[BibT_eX]

[DOI]

IEEE Trans. Dependable Secur. Comput., 2023

Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone.

[BibT_eX]

[DOI]

Int. J. Softw. Informatics, 2023

Preface to the Special Issue on Constraint Solving and Theorem Proving.

[BibT_eX]

[DOI]

Int. J. Softw. Informatics, 2023

Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security.

[BibT_eX]

[DOI]

CoRR, 2023

Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications.

[BibT_eX]

[DOI]

CoRR, 2023

Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems.

[BibT_eX]

[DOI]

CoRR, 2023

Lark: Verified Cross-Domain Access Control for Trusted Execution Environments.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE International Symposium on Software Reliability Engineering, 2023

Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving.

[BibT_eX]

[DOI]

Hao Xu

Proceedings of the 14th Asia-Pacific Symposium on Internetware, 2023

VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Web Services, 2023

2022

A Comprehensive Formalization of AADL with Behavior Annex.

[BibT_eX]

[DOI]

Sci. Program., 2022

PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot.

[BibT_eX]

[DOI]

CoRR, 2022

Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE.

[BibT_eX]

[DOI]

Proceedings of the Internetware 2022: 13th Asia-Pacific Symposium on Internetware, Hohhot, China, June 11, 2022

A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2022

2021

CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2021

Accelerator Virtualization Framework Based on Inter-VM Exitless Communication.

[BibT_eX]

[DOI]

Int. J. Softw. Informatics, 2021

Model learning: a survey of foundations, tools and applications.

[BibT_eX]

[DOI]

Shahbaz Ali

Hailong Sun

Frontiers Comput. Sci., 2021

Apply Formal Methods in Certifying the SyberX High-Assurance Kernel.

[BibT_eX]

[DOI]

Wenjing Xu

Jean Raphael Ngnie Sighom

Chengtao Cao

Lei Wang

Zhe Jiang

Shihong Zou

Proceedings of the Formal Methods - 24th International Symposium, 2021

2020

Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2020

2019

Refinement-Based Specification and Security Analysis of Separation Kernels.

[BibT_eX]

[DOI]

IEEE Trans. Dependable Secur. Comput., 2019

Model Learning: A Survey on Foundation, Tools and Applications.

[BibT_eX]

[DOI]

Shahbaz Ali

Hailong Sun

CoRR, 2019

Combining Model Learning and Model Checking to Analyze Java Libraries.

[BibT_eX]

[DOI]

Shahbaz Ali

Hailong Sun

Proceedings of the Structured Object-Oriented Formal Language and Method, 2019

A Verified Specification of TLSF Memory Management Allocator Using State Monads.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2019

Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS.

[BibT_eX]

[DOI]

Proceedings of the IEEE 22nd International Symposium on Real-Time Distributed Computing, 2019

A Formally Verified Buddy Memory Allocation Model.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Engineering of Complex Computer Systems, 2019

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

A Verified Timsort C Implementation in Isabelle/HOL.

[BibT_eX]

[DOI]

Yu Zhang

CoRR, 2018

An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems.

[BibT_eX]

[DOI]

CoRR, 2018

A Verified Capability-Based Model for Information Flow Security With Dynamic Policies.

[BibT_eX]

[DOI]

Jianwen Sun

Xiang Long

IEEE Access, 2018

Compositional Reasoning for Shared-Variable Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

A survey on formal specification and verification of separation kernels.

[BibT_eX]

[DOI]

Zhibin Yang

Frontiers Comput. Sci., 2017

High-Assurance Separation Kernels: A Survey on Formal Methods.

[BibT_eX]

[DOI]

CoRR, 2017

Formal Verification of Behavioral AADL Models by Stateful Timed CSP.

[BibT_eX]

[DOI]

IEEE Access, 2017

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

2016

Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement.

[BibT_eX]

[DOI]

IEEE Trans. Ind. Informatics, 2016

HV2M: A novel approach to boost inter-VM network performance for Xen-based HVMs.

[BibT_eX]

[DOI]

J. Syst. Softw., 2016

Towards a verified compiler prototype for the synchronous language SIGNAL.

[BibT_eX]

[DOI]

Frontiers Comput. Sci., 2016

Compositional Reasoning for Shared-variable Concurrent Programs.

[BibT_eX]

[DOI]

CoRR, 2016

Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

2015

Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B.

[BibT_eX]

[DOI]

Zhibin Yang

CoRR, 2015

Formal Specification and Verification of Separation Kernels: An Overview.

[BibT_eX]

[DOI]

CoRR, 2015

Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using Event-B.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering, 2015

Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015

2014

PBA4WSSP: a policy-based architecture for web services security processing.

[BibT_eX]

[DOI]

Serv. Oriented Comput. Appl., 2014

MIAPS: A web-based system for remotely accessing and presenting medical images.

[BibT_eX]

[DOI]

Comput. Methods Programs Biomed., 2014

Query dependent multiview features fusion for effective medical image retrieval.

[BibT_eX]

[DOI]

Proceedings of the Proceedings IEEE International Conference on Security, 2014

Formal Modeling of Airborne Software High-Level Requirements Based on Knowledge Graph.

[BibT_eX]

[DOI]

Proceedings of the Knowledge Science, Engineering and Management, 2014

2013

Development of global specification for dynamically adaptive software.

[BibT_eX]

[DOI]

Computing, 2013

A policy-based architecture for web services authentication.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE Symposium on Computers and Communications, 2013

A Web Services Container Supporting QoS Hierarchical Control with Multiple Measurements for Utilization.

[BibT_eX]

[DOI]

Zhe Wang

Proceedings of the IEEE 11th International Conference on Dependable, 2013

2012

A New Re-Ranking Method Using Enhanced Pseudo-Relevance Feedback for Content-Based Medical Image Retrieval.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2012

QDFA: Query-Dependent Feature Aggregation for Medical Image Retrieval.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2012

A hierarchical organization approach of multi-dimensional remote sensing data for lightweight Web Map Services.

[BibT_eX]

[DOI]

Earth Sci. Informatics, 2012

Managing and Collaboratively Processing Medical Image via the Web.

[BibT_eX]

[DOI]

Proceedings of the Web-Age Information Management, 2012

A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems.

[BibT_eX]

[DOI]

Bingyang Zhao

Proceedings of the 15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, 2012

A Policy-Based Architecture for Web Services Security Processing.

[BibT_eX]

[DOI]

Proceedings of the Ninth IEEE International Conference on e-Business Engineering, 2012

Collaborative annotation of medical images via web browser for teleradiology.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Computerized Healthcare, 2012

Automatic RT-Java Code Generation from AADL Models for ARINC653-Based Avionics Software.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual IEEE Computer Software and Applications Conference, 2012

2011

DH4SS: a distributed heuristic for QoS-based service selection.

[BibT_eX]

[DOI]

Int. J. Web Grid Serv., 2011

Building high-speed roads: Improving performance of SOAP processing for cloud services.

[BibT_eX]

[DOI]

Proceedings of the IEEE 6th International Symposium on Service Oriented System Engineering, 2011

Towards Hierarchical Modeling and Analysis of Web Services Choreography.

[BibT_eX]

[DOI]

Proceedings of the Exploring Services Science - Second International Conference, 2011

An AADL-Based Modeling Method for ARINC653-Based Avionics Software.

[BibT_eX]

[DOI]

Proceedings of the 35th Annual IEEE International Computer Software and Applications Conference, 2011

Integrating Business Processes and Business Rules.

[BibT_eX]

[DOI]

Proceedings of the 2011 IEEE Asia-Pacific Services Computing Conference, 2011

FSM4WSR: A Formal Model for Verifiable Web Service Runtime.

[BibT_eX]

[DOI]

Proceedings of the 2011 IEEE Asia-Pacific Services Computing Conference, 2011

Towards Verifying Global Properties of Adaptive Software Based on Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE International Conference on Advanced Information Networking and Applications, 2011

Geospatial Web Service for Remote Sensing Data Visualization.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE International Conference on Advanced Information Networking and Applications, 2011

SCENETester: A Testing Framework to Support Fault Diagnosis for Web Service Composition.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE International Conference on Computer and Information Technology, 2011

2010

Formal Analysis of Behavioural Equivalence for Trustworthy and Composite Web Services.

[BibT_eX]

[DOI]

Proceedings of the Symposia and Workshops on Ubiquitous, 2010

Towards a Graph Grammar Based Verification Approach for Runtime Constrained Evolution of Service-Oriented Architectures.

[BibT_eX]

[DOI]

Proceedings of the Fifth IEEE International Symposium on Service-Oriented System Engineering, 2010

An operational semantics of WS-BPEL based on abstract BPEL machine.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Service-Oriented Computing and Applications, 2010

Towards adaptive web services QoS prediction.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Service-Oriented Computing and Applications, 2010

SEDA4BPEL: A staged event-driven architecture for high-concurrency BPEL engine.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE Symposium on Computers and Communications, 2010

An adaptive heuristic approach for distributed QoS-based service composition.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE Symposium on Computers and Communications, 2010

ACTGIS: A Web-based collaborative tiled Geospatial image map system.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE Symposium on Computers and Communications, 2010

OGC-compatible high-performance web map service for remote sensing data visualization.

[BibT_eX]

[DOI]

Proceedings of the iiWAS'2010, 2010

Medical Image Retrieval with Query-Dependent Feature Fusion Based on One-Class SVM.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Conference on Computational Science and Engineering, 2010

Towards a Formal Verification Approach for Implementation of Web Services Specifications.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE Asia-Pacific Services Computing Conference, 2010

2009

An approach to identifying conversation dependency in service oriented system during dynamic evolution.

[BibT_eX]

[DOI]

Min Liu