Languages

Biblio

Filters: Author is Ming Fu  [Clear All Filters]
2016
Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z.  2016.  A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16), part II, pages 59--79.
2014
Liang H, Feng X, Fu M.  2014.  Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1), pp 3:1-3:55.
2012
Zhang Z, Feng X, Fu M, Shao Z, Li Y.  2012.  A Structural Approach to Prophecy Variables. 9th annual conference on Theory and Applications of Models of Computation.
Liang H, Feng X, Fu M.  2012.  A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12).
2010
Fu M, Zhang Y, Li Y.  2010.  Formal verification of concurrent programs with read-write locks. Frontiers of Computer Science in China. 4(1):13. Download: paper.pdf (317.3 KB); ccprwl_impl.rar (44.96 KB)
2009
Li Y, Zhang Y, Chen Y, Fu M.  2009.  Formal reasoning about lazy-STM programs. submitted to Journal of Computer Science and Technology.  Download: Formal reasoning about lazy-STM programs.pdf (246.32 KB); coq-impl.rar (54.34 KB)
Fu M, Zhang Y, Li Y.  2009.  Formal reasoning about concurrent assembly code with reentrant locks. 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE 2009).  Download: tase2009.pdf (89.95 KB); impl.rar (50.53 KB)
Li Y, Zhang Y, Chen Y, Fu M.  2009.  On the verification of strong atomicity of programs using STM. 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement(SSIRI2009).  Download: SSIRI2009.pdf (269 KB); coq-impl.rar (54.34 KB)