Xinyu Feng

55 papers A* 10A 5B 11C 3Misc 5Journal 12Unranked 8
YearRankTypeTitle / Venue / Authors
2025 — conf
A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model.
ESOP (1)
Weijie Fan, Hongjin Liang, Xinyu Feng, Hanru Jiang
2025 — conf
Verifying Algorithmic Versions of the Lovász Local Lemma.
ESOP (1)
Rongen Lin, Hongjin Liang, Xinyu Feng
2024 Misc conf
Verified Validation for Affine Scheduling in Polyhedral Compilation.
TASE
Xuyang Li, Hongjin Liang, Xinyu Feng
2022 A* conf
Verifying optimizations of concurrent programs in the promising semantics.
PLDI
Junpeng Zha, Hongjin Liang, Xinyu Feng
2021 A* conf
Abstraction for conflict-free replicated data types.
PLDI
Hongjin Liang, Xinyu Feng
2021 J jnl
AutoGR: Automated Geo-Replication with Fast System Performance and Preserved Application Semantics.
Proc. VLDB Endow.
Jiawei Wang, Cheng Li, Kai Ma, Jingze Huo, Feng Yan, Xinyu Feng, Yinlong Xu
2020 J jnl
Formalizing SPARCv8 instruction set architecture in Coq.
Sci. Comput. Program.
Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng
2020 J jnl
Progress of Concurrent Objects.
Found. Trends Program. Lang.
Hongjin Liang, Xinyu Feng
2019 A* conf
Towards certified separate compilation for concurrent programs.
PLDI
Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, Xinyu Feng
2018 Misc ed.
Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China, September 4-6, 2018, Proceedings
SETTA
Xinyu Feng, Markus Müller-Olm, Zijiang Yang
2018 B conf
Modular Verification of SPARCv8 Code.
APLAS
Junpeng Zha, Xinyu Feng, Lei Qiao
2018 C conf
Non-preemptive Semantics for Data-Race-Free Programs.
ICTAC
Siyang Xiao, Hanru Jiang, Hongjin Liang, Xinyu Feng
2018 A* conf
POMP: Protocol Oblivious SDN Programming with Automatic Multi-Table Pipelining.
INFOCOM
Chunhui He, Xinyu Feng
2018 J jnl
Progress of concurrent objects with partial methods.
Proc. ACM Program. Lang.
Hongjin Liang, Xinyu Feng
2017 Misc conf
AndroidLeaker: A Hybrid Checker for Collusive Leak in Android Applications.
SETTA
Zipeng Zhang, Xinyu Feng
2017 Misc conf
Formalizing SPARCv8 Instruction Set Architecture in Coq.
SETTA
Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng
2017 B conf
Mechanized verification of preemptive OS kernels (invited talk).
CPP
Xinyu Feng
2016 — conf
A Practical Verification Framework for Preemptive OS Kernels.
CAV (2)
Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, Zhaohui Li
2016 A* conf
A program logic for concurrent objects under fair scheduling.
POPL
Hongjin Liang, Xinyu Feng
2016 J jnl
An operational happens-before memory model.
Frontiers Comput. Sci.
Yang Zhang, Xinyu Feng
2015 — conf
Disjunctive Information Flow for Communicating Processes.
TGC
Ximeng Li, Flemming Nielson, Hanne Riis Nielson, Xinyu Feng
2015 B conf
Practical Tactics for Verifying C Programs in Coq.
CPP
Jingyuan Cao, Ming Fu, Xinyu Feng
2015 B ed.
Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings
APLAS
Xinyu Feng, Sungwoo Park
2014 J jnl
A temporal programming model with atomic blocks based on projection temporal logic.
Frontiers Comput. Sci.
Xiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng
2014 — conf
Compositional verification of termination-preserving refinement of concurrent programs.
CSL-LICS
Hongjin Liang, Xinyu Feng, Zhong Shao
2014 J jnl
Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations.
ACM Trans. Program. Lang. Syst.
Hongjin Liang, Xinyu Feng, Ming Fu
2013 Misc conf
An Operational Approach to Happens-Before Memory Model.
TASE
Yang Zhang, Xinyu Feng
2013 B conf
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements.
CONCUR
Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao
2013 A* conf
Modular verification of linearizability with non-fixed linearization points.
PLDI
Hongjin Liang, Xinyu Feng
2012 C conf
A Concurrent Temporal Programming Model with Atomic Blocks.
ICFEM
Xiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng
2012 C conf
A Structural Approach to Prophecy Variables.
TAMC
Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li
2012 A* conf
A rely-guarantee-based simulation for verifying concurrent program transformations.
POPL
Hongjin Liang, Xinyu Feng, Ming Fu
2012 — ch.
Mobile Agent Communications.
Mobile Agents in Networking and Distributed Computing
Jian Lu, Xinyu Feng
2012 B conf
Modular Verification of Concurrent Thread Management.
APLAS
Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi
2011 J jnl
Weak Updates and Separation Logic.
New Gener. Comput.
Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
2010 A conf
Parameterized Memory Models and Concurrent Separation Logic.
ESOP
Rodrigo Ferreira, Xinyu Feng, Zhong Shao
2010 B conf
Reasoning about Optimistic Concurrency Using a Program Logic for History.
CONCUR
Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang
2009 J jnl
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.
J. Autom. Reason.
Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
2009 A conf
Deny-Guarantee Reasoning.
ESOP
Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis
2009 A* conf
Local rely-guarantee reasoning.
POPL
Xinyu Feng
2009 B conf
Weak updates and separation logic.
APLAS
Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
2008 A* conf
Certifying low-level programs with hardware interrupts and preemptive threads.
PLDI
Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo
2008 — conf
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.
VSTTE
Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
2007 — conf
An open framework for foundational proof-carrying code.
TLDI
Xinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo
2007 A conf
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.
ESOP
Xinyu Feng, Rodrigo Ferreira, Zhong Shao
2006 A* conf
Modular verification of assembly code with stack-based control abstractions.
PLDI
Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni
2005 A conf
Modular verification of concurrent assembly code with dynamic thread creation and termination.
ICFP
Xinyu Feng, Zhong Shao
2004 J jnl
Path Pruning in Mailbox-based Mobile Agent Communications.
J. Inf. Sci. Eng.
Jiannong Cao, Liang Zhang, Xinyu Feng, Sajal K. Das
2004 J jnl
Reliable message delivery for mobile agents: push or pull?
IEEE Trans. Syst. Man Cybern. Part A
Jiannong Cao, Xinyu Feng, Jian Lu, Henry C. B. Chan, Sajal K. Das
2003 B conf
Adaptive and reliable message delivery for mobile objects.
GLOBECOM
Jiannong Cao, Liang Zhang, Xinyu Feng, Sajal K. Das
2003 B conf
Path Compression in Forwarding-Based Reliable Mobile Agent Communications.
ICPP
Jiannong Cao, Liang Zhang, Xinyu Feng, Sajal K. Das
2002 A conf
Design of Adaptive and Reliable Mobile Agent Communication Protocols.
ICDCS
Jiannong Cao, Xinyu Feng, Jian Lu, Sajal K. Das
2002 J jnl
Mailbox-Based Scheme for Designing Mobile Agent Communication Protocols.
Computer
Jiannong Cao, Xinyu Feng, Jian Lu, Sajal K. Das
2002 B conf
Reliable Message Delivery for Mobile Agents: Push or Pull.
ICPADS
Jiannong Cao, Xinyu Feng, Jian Lu, Henry C. B. Chan, Sajal K. Das
2001 — conf
An Efficient Mailbox-Based Algorithm for Message Delivery in Mobile Agent Systems.
Mobile Agents
Xinyu Feng, Jiannong Cao, Jian Lü, Henry C. B. Chan