头像

徐鸣

副教授(偏重科研)

软件工程学院      

个人资料

  • 部门: 软件工程学院
  • 毕业院校: 华东师范大学
  • 学位: 理学博士
  • 学历: 博士研究生
  • 邮编: 200062
  • 联系电话:
  • 传真:
  • 电子邮箱: mxu@cs.ecnu.edu.cn
  • 办公地址: 理科大楼B1005
  • 通讯地址: 上海市普陀区中山北路3663号

教育经历

工作经历

个人简介

社会兼职

国家自然科学基金委数理学部、信息学部通讯评议人

美国《Mathematical Reviews》评论员

研究方向

目前研究方向:基础算法及其应用


招生类别:学术型硕士生、博士生

欢迎有兴趣从事基础研究的本科生、研究生与我联系,共同探讨!


目前指导学生:

2022级---尤文菁 (硕士生), 李鹏阳 (在职硕士生), 倪海峰 (在职硕士生)

2021级---陆嘉 (硕士生), 陈茜 (在职硕士生), 周俊仁 (在职硕士生)

2020级---李想 (在职硕士生), 纪志成 (在职硕士生)

2019级---傅剑铃 (硕博连读生), 常昊 (在职硕士生)


完成指导学生:

2023届---南艺 (硕士生), 梅敬宜 (硕士生)

2021届---刘珂冰 (本科生, 去向: 公务员)

2020届---厉劲草 (硕士生, 去向: 银行工作), 梅敬宜 (本科生, 优秀学位论文, 去向: 本校读研)

2019届---黄承超 (硕博连读生, 优秀学位论文, 去向: 中科院博士后), 傅剑铃 (本科生, 优秀学位论文, 去向: 本校读研)

2017届---厉劲草 (本科生, 优秀学位论文, 去向: 本校读研)

2016届---吴凯宗 (本科生, 去向: 本校读研)

2015届---王思宁 (本科生, 优秀学位论文, 去向: 德国亚琛工大读研)

2014届---黄唯苇 (本科生, 优秀学位论文, 去向: 微软工作、美国卡内基梅隆大学读研), 黄承超 (本科生, 去向: 本校读研)

招生与培养

开授课程

  本科生课程:

数据结构与算法    离散数学    计算理论基础


  研究生课程:

高级算法    量子计算导引    科技论文写作

科研项目

主持国家自然科学基金面上项目2项、青年项目1项,教育部博士点基金和中国博士后科学基金各一项。

学术成果

[0] J. Fu, C. Huang, Y. Li, J. Mei, M. Xu and L. Zhang (2023): Quantitative Controller Synthesis for Consumption Markov Decision Processes, Information Processing Letters, vol. 180, Article No. 106342.

[1] M. Xu, J. Fu, J. Mei and Y. Deng (2022): An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains, Theoretical Computer Science, vol. 935: 61-81.

[2] M. Xu, J. Fu, J. Mei and Y. Deng (2022): Model Checking QCTL Plus on Quantum Markov Chains, Theoretical Computer Science, vol. 913: 43-72.

[3] M. Xu, J. Mei, J. Guan and N. Yu (2021): Model Checking Quantum Continuous-Time Markov Chains, in Proceedings of the 32nd International Conference on Concurrency Theory (CONCUR 2021), LIPIcs, vol. 203, Article No. 13, pp. 1-17, Schloss Dagstuhl.

[4] M. Xu, C. Huang and Y. Feng (2021): Measuring the Constrained Reachability in Quantum Markov Chains, Acta Informatica, vol. 58(6): 653-674.

[5] Y. Sun, M. Xu and Y. Deng (2021): An Optimal Quantum Error-Correcting Procedure Using Quantifier Elimination, Quantum Information Processing, vol. 20, Article No. 170.

[6] M. Xu and Y. Deng (2020): Time-bounded Termination Analysis for Probabilistic Programs with Delays, Information and Computation, vol. 275, Article No. 104634.

[7] P. Wang, H. Fu, K. Chatterjee, Y. Deng and M. Xu (2020): Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time, in Proceedings of the ACM on Programming Languages, vol. 4, issue POPL, Article No. 25, pp. 1-30, ACM.

[8] C. Huang, M. Xu and Z. Li (2020): A Conflict-Driven Solving Procedure for Poly-Power Constraints, Journal of Automated Reasoning, vol. 64(1), 1-20.

[9] C. Huang, J. Li, M. Xu and Z. Li (2018): Positive Root Isolation for Poly-Powers by Exclusion and Differentiation, Journal of Symbolic Computation, vol. 85, 148-169.

[10] J. Li, C. Huang, M. Xu and Z. Li (2016): Positive Root Isolation for Poly-Powers, in Proc. 41st ISSAC, pp. 325-332, ACM.

[11] M. Xu, L. Zhang, D. N. Jansen, H. Zhu and Z. Yang (2016): Multiphase Until Formulas over Markov Reward Models: An Algebraic Approach, Theoretical Computer Science, vol. 611, 116-135.

[12] M. Xu, C. Huang, Z. Li and Z. Zeng (2016): Analyzing Ultimate Positivity for Solvable Systems, Theoretical Computer Science, vol. 609, part 2: 395-412.

[13] M. Xu, Z. Li and L. Yang (2015): Quantifier Elimination for a Class of Exponential Polynomial Formulas, Journal of Symbolic Computation, vol. 68, part 1: 146-168.

[14] M. Xu and Z. Li (2013): Symbolic Termination Analysis of Solvable Loops, Journal of Symbolic Computation, vol. 50: 28-49.

[15] Y. Gao, M. Xu, N. Zhan and L. Zhang (2013): Model Checking Conditional CSL for Continuous-Time Markov Chains, Information Processing Letters, vol. 113(1-2): 44-50.

荣誉及奖励

10 访问

相关教师