| 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 | 111 | 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 | 90 | 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 | 76 | 2012 |
| VSync: push-button verification and optimization for synchronization primitives on weak memory models J Oberhauser, RLDL Chehab, D Behrens, M Fu, A Paolillo, L Oberhauser, ... Proceedings of the 26th ACM International Conference on Architectural …, 2021 | 46 | 2021 |
| 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 | 46 | 2019 |
| 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 | 40 | 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 | 17 | 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 | 16 | 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 | 14 | 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 | 9 | 2022 |
| Formalizing SPARCv8 instruction set architecture in Coq J Wang, M Fu, L Qiao, X Feng Science of Computer Programming 187, 102371, 2020 | 7 | 2020 |
| 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 | 6 | 2023 |
| 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 | 5 | 2021 |
| Homomorphism resolving of xpath trees based on automata M Fu, Y Zhang Asia-Pacific Web Conference, 821-828, 2007 | 5 | 2007 |
| {BWoS}: Formally Verified Block-based Work Stealing for Parallel Processing J Wang, B Trach, M Fu, D Behrens, J Schwender, Y Liu, J Lei, V Vafeiadis, ... 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2023 | 4 | 2023 |
| 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 | 4 | 2019 |
| 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 | 4 | 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 | 4 | 2009 |
| 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 | 3 | 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 | 3 | 2011 |
Xinyu FengNanjing UniversityVerified email at nju.edu.cn
