An Efficient Mailbox-Based Algorithm for Message Delivery in Mobile Agent Systems. - Xinyu Feng 001; Jiannong Cao 001; Jian Lü 001; Henry C. B. Chan (Mobile Agents, 2001)

Design of Adaptive and Reliable Mobile Agent Communication Protocols. - Jiannong Cao 001; Xinyu Feng 001; Jian Lu 001; Sajal K. Das 001 (ICDCS, 2002)

Mailbox-Based Scheme for Designing Mobile Agent Communication Protocols. - Jiannong Cao 001; Xinyu Feng 001; Jian Lu 001; Sajal K. Das 001 (Computer, 2002)

Adaptive and reliable message delivery for mobile objects. - Jiannong Cao 001; Liang Zhang 027; Xinyu Feng 001; Sajal K. Das 001 (GLOBECOM, 2003)

Path Compression in Forwarding-Based Reliable Mobile Agent Communications. - Jiannong Cao 001; Liang Zhang 027; Xinyu Feng 001; Sajal K. Das 001 (ICPP, 2003)

Path Pruning in Mailbox-based Mobile Agent Communications. - Jiannong Cao 001; Liang Zhang 027; Xinyu Feng 001; Sajal K. Das 001 (J. Inf. Sci. Eng., 2004)

Reliable message delivery for mobile agents: push or pull? - Jiannong Cao 001; Xinyu Feng 001; Jian Lu 001; Henry C. B. Chan; Sajal K. Das 001 (IEEE Trans. Syst. Man Cybern. Part A, 2004)

Modular verification of concurrent assembly code with dynamic thread creation and termination. - Xinyu Feng 001; Zhong Shao 001 (ICFP, 2005)

Modular verification of assembly code with stack-based control abstractions. - Xinyu Feng 001; Zhong Shao 001; Alexander Vaynberg; Sen Xiang; Zhaozhong Ni (PLDI, 2006)

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. - Xinyu Feng 001; Rodrigo Ferreira; Zhong Shao 001 (ESOP, 2007)

An open framework for foundational proof-carrying code. - Xinyu Feng 001; Zhaozhong Ni; Zhong Shao 001; Yu Guo (TLDI, 2007)

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. - Xinyu Feng 001; Zhong Shao 001; Yu Guo; Yuan Dong (VSTTE, 2008)

Deny-Guarantee Reasoning. - Mike Dodds; Xinyu Feng 001; Matthew J. Parkinson; Viktor Vafeiadis (ESOP, 2009)

Local rely-guarantee reasoning. - Xinyu Feng 001 (POPL, 2009)

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. - Xinyu Feng 001; Zhong Shao 001; Yu Guo; Yuan Dong (J. Autom. Reason., 2009)

Reasoning about Optimistic Concurrency Using a Program Logic for History. - Ming Fu; Yong Li; Xinyu Feng 001; Zhong Shao 001; Yu Zhang 086 (CONCUR, 2010)

Parameterized Memory Models and Concurrent Separation Logic. - Rodrigo Ferreira; Xinyu Feng 001; Zhong Shao 001 (ESOP, 2010)

Weak Updates and Separation Logic. - Gang Tan; Zhong Shao 001; Xinyu Feng 001; Hongxu Cai (New Gener. Comput., 2011)

Mobile Agent Communications. - Jian Lu 001; Xinyu Feng 001 (Mobile Agents in Networking and Distributed Computing, 2012)

Modular Verification of Concurrent Thread Management. - Yu Guo; Xinyu Feng 001; Zhong Shao 001; Peizhi Shi (APLAS, 2012)

A Concurrent Temporal Programming Model with Atomic Blocks. - Xiaoxiao Yang; Yu Zhang 086; Ming Fu; Xinyu Feng 001 (ICFEM, 2012)

A rely-guarantee-based simulation for verifying concurrent program transformations. - Hongjin Liang 001; Xinyu Feng 001; Ming Fu (POPL, 2012)

A Structural Approach to Prophecy Variables. - Zipeng Zhang; Xinyu Feng 001; Ming Fu; Zhong Shao 001; Yong Li (TAMC, 2012)

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. - Hongjin Liang 001; Jan Hoffmann 002; Xinyu Feng 001; Zhong Shao 001 (CONCUR, 2013)

Modular verification of linearizability with non-fixed linearization points. - Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2013)

An Operational Approach to Happens-Before Memory Model. - Yang Zhang; Xinyu Feng 001 (TASE, 2013)

Compositional verification of termination-preserving refinement of concurrent programs. - Hongjin Liang 001; Xinyu Feng 001; Zhong Shao 001 (CSL-LICS, 2014)

A temporal programming model with atomic blocks based on projection temporal logic. - Xiaoxiao Yang; Yu Zhang 086; Ming Fu; Xinyu Feng 001 (Frontiers Comput. Sci., 2014)

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. - Hongjin Liang 001; Xinyu Feng 001; Ming Fu (ACM Trans. Program. Lang. Syst., 2014)

Practical Tactics for Verifying C Programs in Coq. - Jingyuan Cao; Ming Fu; Xinyu Feng 001 (CPP, 2015)

Disjunctive Information Flow for Communicating Processes. - Ximeng Li 001; Flemming Nielson; Hanne Riis Nielson; Xinyu Feng 001 (TGC, 2015)

A Practical Verification Framework for Preemptive OS Kernels. - Fengwei Xu; Ming Fu; Xinyu Feng 001; Xiaoran Zhang; Hui Zhang; Zhaohui Li (CAV (2), 2016)

A program logic for concurrent objects under fair scheduling. - Hongjin Liang 001; Xinyu Feng 001 (POPL, 2016)

An operational happens-before memory model. - Yang Zhang; Xinyu Feng 001 (Frontiers Comput. Sci., 2016)

Mechanized verification of preemptive OS kernels (invited talk). - Xinyu Feng 001 (CPP, 2017)

AndroidLeaker: A Hybrid Checker for Collusive Leak in Android Applications. - Zipeng Zhang; Xinyu Feng 001 (SETTA, 2017)

Non-preemptive Semantics for Data-Race-Free Programs. - Siyang Xiao; Hanru Jiang; Hongjin Liang 001; Xinyu Feng 001 (ICTAC, 2018)

POMP: Protocol Oblivious SDN Programming with Automatic Multi-Table Pipelining. - Chunhui He; Xinyu Feng 001 (INFOCOM, 2018)

Progress of concurrent objects with partial methods. - Hongjin Liang 001; Xinyu Feng 001 (Proc. ACM Program. Lang., 2018)

Towards certified separate compilation for concurrent programs. - Hanru Jiang; Hongjin Liang 001; Siyang Xiao; Junpeng Zha; Xinyu Feng 001 (PLDI, 2019)

A Lightweight Dynamic Enforcement of Privacy Protection for Android. - Zipeng Zhang; Ming Fu; Xin-Yu Feng 001 (J. Comput. Sci. Technol., 2019)

Progress of Concurrent Objects. - Hongjin Liang 001; Xinyu Feng 001 (Found. Trends Program. Lang., 2020)

Modular Verification of SPARCv8 Code. - Junpeng Zha; Xin-Yu Feng 001; Lei Qiao 002 (J. Comput. Sci. Technol., 2020)

Formalizing SPARCv8 instruction set architecture in Coq. - Jiawei Wang; Ming Fu; Lei Qiao 002; Xinyu Feng 001 (Sci. Comput. Program., 2020)

Abstraction for conflict-free replicated data types. - Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2021)

Verifying Contextual Refinement with Ownership Transfer. - Zhao-Hui Li; Xin-Yu Feng 001 (J. Comput. Sci. Technol., 2021)

AutoGR: Automated Geo-Replication with Fast System Performance and Preserved Application Semantics. - Jiawei Wang; Cheng Li 001; Kai Ma; Jingze Huo; Feng Yan 001; Xinyu Feng 001; Yinlong Xu (Proc. VLDB Endow., 2021)

Verifying optimizations of concurrent programs in the promising semantics. - Junpeng Zha; Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2022)

Verified Validation for Affine Scheduling in Polyhedral Compilation. - Xuyang Li; Hongjin Liang 001; Xinyu Feng 001 (TASE, 2024)

A program logic for obstruction-freedom. - Zhao-Hui Li; Xin-Yu Feng 001 (Frontiers Comput. Sci., 2024)

A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. - Weijie Fan; Hongjin Liang 001; Xinyu Feng 001; Hanru Jiang (ESOP (1), 2025)

Verifying Algorithmic Versions of the Lovász Local Lemma. - Rongen Lin; Hongjin Liang 001; Xinyu Feng 001 (ESOP (1), 2025)