Ming Fu
Ming Fu
Huawei Dresden Research Center
Dirección de correo verificada de - Página principal
Citado por
Citado por
A practical verification framework for preemptive OS kernels
F Xu, M Fu, X Feng, X Zhang, H Zhang, Z Li
International Conference on Computer Aided Verification, 59-79, 2016
Reasoning about optimistic concurrency using a program logic for history
M Fu, Y Li, X Feng, Z Shao, Y Zhang
CONCUR 2010-Concurrency Theory: 21th International Conference, CONCUR 2010 …, 2010
A rely-guarantee-based simulation for verifying concurrent program transformations
H Liang, X Feng, M Fu
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2012
Using concurrent relational logic with helpers for verifying the AtomFS file system
M Zou, H Ding, D Du, M Fu, R Gu, H Chen
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 259-274, 2019
VSync: push-button verification and optimization for synchronization primitives on weak memory models
J Oberhauser, RLL Chehab, D Behrens, M Fu, A Paolillo, L Oberhauser, ...
Proceedings of the 26th ACM International Conference on Architectural …, 2021
Rely-guarantee-based simulation for compositional verification of concurrent program transformations
H Liang, X Feng, M Fu
ACM Transactions on Programming Languages and Systems (TOPLAS) 36 (1), 1-55, 2014
Practical tactics for verifying C programs in Coq
J Cao, M Fu, X Feng
Proceedings of the 2015 Conference on Certified Programs and Proofs, 97-108, 2015
A structural approach to prophecy variables
Z Zhang, X Feng, M Fu, Z Shao, Y Li
Theory and Applications of Models of Computation: 9th Annual Conference …, 2012
Clof: A compositional lock framework for multi-level NUMA systems
RL de Lima Chehab, A Paolillo, D Behrens, M Fu, H Härtig, H Chen
Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles …, 2021
{BBQ}: A Block-based Bounded Queue for Exchanging Data and Profiling
J Wang, D Behrens, M Fu, L Oberhauser, J Oberhauser, J Lei, G Chen, ...
2022 USENIX Annual Technical Conference (USENIX ATC 22), 249-262, 2022
Formalizing SPARCv8 instruction set architecture in Coq
J Wang, M Fu, L Qiao, X Feng
Science of Computer Programming 187, 102371, 2020
Verifying and optimizing the HMCS lock for Arm servers
J Oberhauser, L Oberhauser, A Paolillo, D Behrens, M Fu, V Vafeiadis
Networked Systems: 9th International Conference, NETYS 2021, Virtual Event …, 2021
Homomorphism resolving of xpath trees based on automata
M Fu, Y Zhang
Asia-Pacific Web Conference, 821-828, 2007
Formal reasoning about lazy-STM programs
Y Li, Y Zhang, YY Chen, M Fu
Journal of Computer Science and Technology 25 (4), 841-852, 2010
Formal reasoning about concurrent assembly code with reentrant locks
M Fu, Y Zhang, Y Li
2009 Third IEEE International Symposium on Theoretical Aspects of Software …, 2009
A lightweight dynamic enforcement of privacy protection for android
ZP Zhang, M Fu, XY Feng
Journal of Computer Science and Technology 34, 901-923, 2019
A concurrent temporal programming model with atomic blocks
X Yang, Y Zhang, M Fu, X Feng
International Conference on Formal Engineering Methods, 22-37, 2012
Certifying the concurrent state table implementation in a surgical robotic system (extended version)
Y Kouskoulas, F Ming, Z Shao, P Kazanzides
Technical report, Yale University, 2011
AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM
M Beck, K Bhat, L Stričević, G Chen, D Behrens, M Fu, V Vafeiadis, ...
Proceedings of the 28th ACM International Conference on Architectural …, 2023
On the Verification of Strong Atomicity in Programs using STM
Y Li, Y Zhang, Y Chen, M Fu
2009 Third IEEE International Conference on Secure Software Integration and …, 2009
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20