导航

  • 个人资料
  • 个人概况
  • 研究方向
  • 招生与培养
  • 开授课程
  • 科研项目
  • 学术成果
  • 荣誉及奖励
头像

张民

相关教师

个人资料

  • 部门： 软件工程学院
  • 性别： 男
  • 专业技术职务： 教授/博士生导师/系主任
  • 毕业院校： 日本北陆先端科学技术大学院大学
  • 学位： 博士
  • 学历： 研究生
  • 联系电话： 1381895
  • 电子邮箱： zhangmin@sei.ecnu.edu.cn
  • 办公地址： 理科大楼B1117,021-62235020
  • 通讯地址： 上海市普陀区中山北路3663号理科大楼B1117室
  • 邮编： 200062
  • 传真：

教育经历

2008.04-2011.09：日本北陆先端科学技术大学院大学（JAIST） 

                                   信息科学学院 (School of Information Science)，软件科学博士

2005.09-2008.03：上海交通大学，计算机科学与工程系，BASICS实验室，软件硕士

2001.09-2005.06：山东师范大学，计算机科学与技术，本科


工作经历

2021.01 -    至今：  华东师范大学，软件工程学院，教授

2014.11-2020.12：华东师范大学，软件学院，副教授

2011.10-2014.10：日本北陆先端科学技术大学院大学，博士后研究员


个人简介

研究方向：可信软件、可信人工智能和分布式系统。研究受到国家自然基金委国际合作项目（中以）、面上项目与青年项目、华为全球创新研究计划(HIRP)、国家留学基金委以及法国高等教育署等国家级和国际合作项目的资助，2019年入选中法“蔡元培”人才培养计划，2019-2020年入选法国尼斯大学高级访问教授计划，目前担任中法Inria-ECNU可信物联网联合团队中方负责人。在CAV、NuerIPS、AAAI、OOPSLA、ASE、RTSS、DAC、FSE、ISSTA、CVPR、DATE等国际旗舰会议以及TCS、SCP、IEEE Trans等权威期刊发表论文70余篇。获得第26届IEEE亚太软件工程会议APSEC唯一最佳论文奖，FSE 2020 (CCF-A)和RE2019会议(CCF-B)最佳论文提名奖。

心有所信，方能行远！

社会兼职

I actively particiapte into the following events: 

    Frontiers of Computer Science, 2014

    IEICE Transactions on Information & System, 2014

    IEICE Transactions on Information & System, 2013

    IEICE Transactions on Information & System, 2012

    SAS 2014

    FoSSaCS 2013

研究方向

软件的形式化建模与验证，程序语言设计与分析，Maude, Rewriting Logic等.

当前主要研究的方向包括：

1. 深度学习模型的可靠性研究：如神经网络鲁棒性验证与训练，强化学习系统的可靠性训练与验证

2. 区块链分布式协议验证与测试，智能合约验证与测试

招生与培养

CALL FOR PEOPLE (CFP)

课题组目前博士生5人，学术硕士研究生7人，专业硕士研究生9人。

欢迎优秀的学生加入TIC LAB，也长期招聘博士后和专职副研究员。也欢迎高年级的本科生来实验室实习实践！希望你：

  1. 能够承担很大的压力，

  2. 对科研有很大的兴趣，

  3. 有做好一件事的勇气。


2024年计划招收一名专职副研究员或博士后研究员，方向为机器学习和形式化验证领域，提供有竞争力的工资待遇和国际访学资助！有兴趣者可发简历至 zhangmin@sei.ecnu.edu.cn


初种根时，只管栽培灌溉，勿作枝想，勿作叶想，勿作花想，勿作实想。

悬想何益?但不忘栽培之功，怕没有枝叶花实?


Awards for Students:  

  1. 郅大鹏同学（D3）的论文Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems”被第36届CAV（CCF-A类）会议录用。

  2. [2023.12] 郅大鹏同学（D3）的论文“Robustness Verification of Deep Reinforcement Learning Based Control Systems using Reward Martingales”被第38届AAAI（CCF-A类）会议录用。

  3. [2023.10] 田家旭同学（M3）获得国家奖学金。

  4. [2023.09] 田家旭（M3）、郅大鹏（D3）同学的论文“Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training ” 被第25届形式化方法国际权威会议VMCAI 2024（CCF-B类）录用。

  5. [2023.09] 田家旭（M3）、郅大鹏（D3）同学的论文“Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural Networks”被第37届人工智能领域顶级会议NeurIPS 2023（CCF-A类）录用。

  6. [2023.05] 薛志一（M2）、张兆迪（D4）、吴旖婷（M3）三位同学的论文A Tale of Two Approximations: Tightening Over-Approximation for  DNN Robustness Verification via Under-Approximation被ISSTA 2023（CCF-A类）录用。

  7. [2023.02] 张兆迪（D4）、薛志一（M2）、陈洋（M2）三位同学的论文Boosting Verified Training for Robust Image Classifications via Abstraction被CVPR 2023（CCF-A类）录用。

  8. [2022.12] 郭省吾（M2）、周孜为（B3）同学的论文OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks被国际顶级会议第29届TACAS 2023（CCF-B类）录用。

  9. [2022.12]2019级硕士金鹏同学（M3）的硕士论文《基于抽象域训练的可验证强化学习》入选华东师范大学优秀硕士毕业论文。

  10. [2022.07] Our work 'Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks', has been acccepted by ASE 2022  (CCF-A)

  11. [2022.07] Our joint work 'QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks', with Fu Song (ShanghaiTech University) et. al, has been acccepted by ASE 2022  (CCF-A)

  12. [2022.07] Our joint work 'Neural Network Verification with Proof Production', with Omri Isac, Clark Barrett and Guy Katz, has been acccepted by FMCAD 2022  (CCF-C)

  13. [2022.07] Our joint work 'Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems', with Dr. Si Liu, Peter Olveczky, Jose Meseguer, David Basin, has been acccepted by OOPSLA 2022 (CCF-A)

  14. [2022.05] 金鹏、田家旭、郅大鹏三位同学的论文Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning被形式化领域顶级会议CAV 2022（CCF-A类）录用！

  15. [2021.10] I will serve as the PC chair for ICFEM 2022,one of the premier conferneces on formal methods. ICFEM 2022 is to going to be held on Oct. 24-27,2022 in Madrid, Spain. 

  16. [2021.08] 2021级硕士研究生郭省吾同学的论文Eager Falsification For Accelerating Robustness Verification of Deep Neural Networks被第32届国际软件过程可靠性会议ISSRE（CCF-B类）录用。

  17. [2021.07] I will serve as TPC member for the Track D1 of DATE 2022. Submit your contributions by Step. 12!

  18. [2021.04] I will serve as PC member of FoMLAS 2021, a satellite workshop of CAV 2021！

  19. [2020.12] I will co-chair TASE 2021 with Kazuhiro Ogata from 08/25 to 08/27 in 2021！

  20. [2020.12] 2020级硕士研究生吴旖婷同学的论文被人工智能顶级会议AAAI'21录用！ 

  21. [2020.09] 2016级硕士研究生高飞同学毕业论文入选华东师范大学信息学部优秀毕业论文！

  22. [2020.05] 2016级硕士研究生迟晓彤同学被评委上海市优秀毕业生！

  23. [2020.05] 2020年入选法国蔚蓝海岸大学“Senior Professor”外籍学者访问项目。

  24. [2020.03] ECNU-Inria Associated Team for FM4CPS project is granted. (ECNU-Inria FM4CPS联合团队获得Inria资助）

  25. [2019.12] 迟晓彤同学的论文“An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems” 获APSEC2019最佳论文奖。

  26. [2019.11] 2017级硕士研究生高飞同学的学术论文“Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint”被DATE2020会议接收。

  27. [2019.07] 2019年中法“蔡元培”交流合作项目获得国家留学基金委资助，中方负责人。

  28. [2019.06] 2019年入选法国蔚蓝海岸大学“Senior Professor”外籍学者访问项目。

  29. [2019.01] 2016级硕士研究生钱佳琪同学被评为华东师范大学优秀毕业生。

  30. [2019.01] 2016级硕士研究生钱佳琪同学的学术论文“KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs”被FASE 2019接收。

  31. [2018.11] 2016级硕士研究生唐玮同学获得国家励志奖学金，祝贺唐玮。

  32. [2018.08] 2015级博士研究生朱晓冉同学的学术论文“Towards a unified executable formal automobile OS kernel and its applications.”被IEEE Transactions on Reliability国际期刊录用。

  33. [2018.08] 国家自然科学基金面上项目 “基于时钟约束建模语言CCSL的实时嵌入式系统形式化验证与分析” 2019.01.01~2022.12.31, 主持人。

  34. [2018.08] 实验室获批华为OPEN HIRP项目资助。

  35. [2018.03] 实验室2018年度中法“徐光启”项目--基于SMT技术的时钟约束描述语言的形式化验证与分析 获批，中方负责人.

  36. [2017.11] 2015级硕士研究生应云辉同学的学术论文“基于SMT的时钟约束语言CCSL的形式化分析方法与工具”被软件学报录用。

  37. [2017.03] 2015级硕士研究生应云辉同学的学术论文“Towards SMT-based LTL Model Checking of Clock Constraint Specification Language for Real-Time and Embedded Systems”被LCTES 2017会议接收。

  38. [2017.03] 2014级硕士研究生代风同学被评为“校优秀毕业生”，祝贺代风。

  39. [2015.08] 国家自然科学基金青年项目 “基于模型检测的高可靠性软件动态更新的设计与验证” 2016.01.01~2018.12.31, 主持人

开授课程

科研项目

课题组主要研究的方向包括如下几个方面，里面充满了各种挑战性问题，欢迎有兴趣的同学或者科研人员共同探讨，一起合作。欢迎发邮件至 zhangmin@sei.ecnu.edu.cn 交流探讨。

1. 基于抽象学习技术的可信强化学习方法研究

    研究如何保证强化学习系统的安全可信，如何验证一个强化学习系统满足预设的安全需求？

    形式化验证强化学习系统的难点：

    i) 系统包含难以验证的神经网络模型

   ii) 系统包含非线性动力学方程，难以验证

  iii) 系统状态空间多是无限的，难以被直接利用模型检测技术验证

   课题组提出基于抽象的强化学习技术（请参考我们前期发表的论文CAV2022），开发了原型工具，工具连接：https://github.com/aptx4869tjx/RL_verification，目前该方向比较有前途的研究方向：

   (1) 抽象强学学习系统的可达性分析技术，我们提出了一种分段线性神经网络控制器的训练与验证方法，发表于NeurIPS2023。

   (2) 抽象强化学习系统的鲁棒性：概率鲁棒（probabilistic robustness），一种可证明的鲁棒量化指标，避免鲁棒仅仅依赖仿真测试的局限，如何计算DRL系统鲁棒的概率？

   (3) 抽象强化学习系统的概率模型检测问题，对于非确定action的DRL系统，如何利用概率模型检测验证系统需求的概率可满足性。

   (4) 当前最简单的抽象是把每个输入映射到一个区间，神经网络接收区间为输入，大大降低验证的空间，但是依然面临组合爆炸问题，如何进一步压缩验证空间，同时保证系统的performance不会受到影响？


2. 基于抽象的高鲁棒性深度学习技术，面向任务逻辑需求的机器学习技术

   (1) 研究如何对训练数据抽象以提升神经网络的鲁棒性，实验结果已经说明了该方向的可行性，我们利用抽象的方法在图片分类方面训练鲁棒的图片分类器的工作已取得初步的进展，相关的成果发表在2023年CVPR国际会议上。

   (2) 研究如何根据学习对象的需求，把需求(property)引入训练过程，确保训练好的模型自动满足预设的需求，实现模型的可信训练？


3. 神经网络的鲁棒性验证中的线性近似技术

    通过对激活函数线性近似以提升神经网络验证的鲁棒性是当前主流的验证技术。然而如何减少上近似带来的误差提升验证结果的精度是当前该技术迫切需要解决的问题。

    现有的关于线性近似的tightness的定义并不能保证近似是tight的，存在大量的反例。

    本课题研究什么是tight over-approximation，如何定义tightness，如何实现更tight的上近似？

    (1)目前已经提出了一种细粒度近似技术（发表在AAAI2021），对应的工具https://github.com/VivianWu0512/DeepCert

    (2) 提出了一种针对非负网络的可证明最tight的近似技术（provably tight），发表在ASE2022上。对应的工具链接：

         https://github.com/WitnessNR/NeWise

          然而，对于混合权重的神经网络，近似误差的极限在哪里，我们最新的成果发表在ISSTA2023上。？

    (3) 神经网络验证的复杂性分析，如何证明sigmoid-like的神经网络验证问题也是可判定的？复杂度是多少？

    (4) 神经网络语义鲁棒的验证，如何针对某种语义扰动，如旋转、扭曲等几何扰动，下雨、阴天等天气噪声，证明模型在各种情况下的鲁棒性？构建不同的验证库？

实验室在遮挡扰动方面的验证工作发表在2023年形式化领域顶级的国际会议TACAS上。其余语义扰动的鲁棒性验证研究持续进展中。。。

学术成果

2024:

  1. Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong, Min Zhang

    Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems

    The 36th CAV 2024 (CCF-A) , Accepted

  2. Haoze Wu,  Omri Isac, ..., Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett

    Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

    The 36th CAV 2024  (CCF-A), Accepted

  3. Dapeng Zhi, Peixin Wang, Cheng Chen, Min Zhang

     Robustness Verification of Deep Reinforcement Learning Based Control Systems using Reward Martingales

    The 38th AAAI, 2024,  (CCF-A, Link)

  4. Zhaohui Wang, Min Zhang, Jingran Yang, Bojie Shao, Min Zhang

    MAFT: Efficient Model-Agnostic Fairness Testing for Deep Neural Networks via Zero-Order Gradient Search

    The 46th ICSE, 2024, Accepted (CCF-A, Technical Track)

  5. Zhiyi Xue, Liangguo Li, Senyue Tian, Xiaohong Chen, Pingping Li, Liangyu Chen, Tingting Jiang, Min Zhang

    Domain Knowledge is All You Need: A Field Deployment of  LLM-Powered Test Case Generation in FinTech Domain

    The 46th ICSE, 2024, Accepted (CCF-A, Poster Track)

  6. Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Guy Katz, Min Zhang:

    Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training

    The 25th VMCAI, 2024,  Vol. 14500, pp. 73 - 97, LNCS, Springer (CCF-B, link)

  7. Yuanrui Zhang, Frederic Mallet, Min Zhang, Zhiming LiuMin Zhang

    Specification and Verification of Multi-clock Systems using a Temporal Logic with Clock Constraints

    Formal Aspects of Computing, Volume 36 Issue 2, 2024, (CCF-B, Link)

  8. Xiaohong Chen, Zhi Ji, Min Zhang, Frédéric Mallet, Xiaoshan Liu, Tingliang Zhou

    A Scalable Approach to Detecting SafetyRequirements Inconsistencies for Railway Systems

    IEEE Transactions on Intelligent Transportation Systems (to appear)

  9. Liangyu Chen, Chen Wang, Cheng Chen, Caidie Huang, Xiaohong Chen, Min Zhang

    HomeGuard: A Lightweight SMT-Based Conflict Analysis for Trigger-Action Programming

    IEEE Internet of Things (IoT) Journal, 2024, Accepted

    10. 2023:

  10. Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Cheng Chen, Min Zhang:

    Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural Networks

    The 37th NeurIPS, 2023,  Accepted (CCF-A, Link)

  11. Zhiyi Xue, Si Liu, Zhaodi Zhang, Yiting Wu, Min Zhang:

    A Tale of Two Approximations: Tightening Over-Approximation for  DNN Robustness Verification via Under-Approximation

    The 32nd ISSTA, 2023, pp. 1182-1194, ACM. (CCF-A, Link)

  12. Zhaodi Zhang, Zhiyi Xue, Yang Chen, Si Liu, Yueling Zhang, Jing Liu, Min Zhang:

    Boosting Verified Training for Robust Image Classifications via Abstraction

    The CVPR, 2023 pp. 16251-16260,  (CCF-A, Link)

  13. Xiaohong Chen, Juan Zhang, Zhi Jin, Min Zhang, Tong Li, Xiang Chen, Tingliang Zhou:

    Empowering Domain Experts with Formal Methods for Consistency Verification of Safety Requirements

    The IEEE Transactions on Intelligent Transportation Systems, 2023 (JCR Q1)

  14. Ming Hu, Jun Xia, Min Zhang, Xiaohong Chen, Frederic Mallet, Mingsong Chen:

    Automated Synthesis of Safe Timing Behaviors for Requirements Models using CCSL

    The IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023 (CCF-A, link)

  15. Ming Hu, E Cao, Hongbing Huang, Min Zhang, Xiaohong Chen, Mingsong Chen:

    AIoTML: A Unified Modeling Language for AIoT-Based Cyber-Physical Systems

    The IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023 (CCF-A, link)

  16. Xingwu Guo, Ziwei Zhou,  Yueling Zhang, Katz Guy, Min Zhang:

    OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks

    The 29th TACAS, pp. 208-226, LNCS, Springer, 2023  (CCF-B, Link)

  17. Xinping Wang, Liangyu Chen, Min Zhang:

    Deep Attentive Model for Knowledge Tracing    

    The 37th AAAI, pp. 10192-10199, AAAI, 2023 (CCF-A, Link)

    18. 2022:

  18. Min Zhang:

    Abstraction-Based Training and Verification of Safe Deep Reinforcement Learning Systems (extended abstract)

    The 8th SETTA, vol. 13649, LNCS, Springer, 2022  (CCF-C, PDF)

  19. Zhaodi Zhang, Yiting Wu, Si Liu, Jing Liu*, Min Zhang*:

    Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks.

    The 37th ASE, 2022, ACM (CCF-A, PDF)

  20. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Min Zhang, Taolue Chen, Jun Sun:

    QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks.

    The 37th ASE 2022, ACM (CCF-A)

  21. Peng Jin, Jiaxu Tian, Dapeng Jin, Xuejun Wen, Min Zhang*: 

    Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning.

    The 34th CAV, pp. 219-238, vol. 13371, Springer, 2022 (CCF-A, PDF, Slides, Video)

  22. Si Liu, Peter C. Olveczky, Jose Meseguer, Min Zhang, David Basin: 

    Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems. 

    OOPSLA 2022, ACM (CCF-A, PDF)

  23. Ming Hu, Min Zhang, Frederic Mallet, Xin Fu, Mingsong Chen

    Accelerating Reinforcement Learning-based CCSL Specification Synthesis Using Curiosity-Driven Exploration.

    IEEE Transactions on Computers. (CCF-A, URL)

  24. Omri Isac, Clark Barrett, Min Zhang, Guy Katz : 

    Neural Network Verification with Proof Production.

    FMCAD 2022, IEEE. (CCF-C, PDF)

  25. Zhaodi Zhang, Jing Liu, Min Zhang, Haiying Sun: 

    Efficient Robustness Verification of the Neural Networks in Smart IoT Devices.

    The Computer Journal. (CCF-B, PDF)

  26. Peng Jin, Yang Wang, Min Zhang*: 

    Efficient LTL Model Checking of Deep Reinforcement Learning Systems using Policy Extraction.

    The 34th SEKE, 2022 (CCF-C, PDF)

    27. 2021:

  27. Yiting Wu, Min Zhang*:

    Tightening Robustness Verification of Convolutional Neural Networks with Fine-Grained Linear Approximation.

    The 35th AAAI, pp. 11674-11681, AAAI (CCF-A, LINK).

  28. Jifeng He, Geguang Pu, Mingsong Chen, Min Zhang*, Weikai Miao:

    Toward trustworthy human-cyber-physical systems: Theories, methods, and applications.

    70 Years of Excellence, Science Digest, 54, AAAS

  29.  Ming Hu, Jiepin Ding, Min Zhang, Frederic Mallet and Mingsong Chen: 

    Enumeration and Deduction Driven Co-Synthesis of CCSL Specifications Using Reinforcement Learning. 

    The 42th RTSS, pp. 227-239, IEEE, 2021 (CCF-A)

  30. 边寒, 陈小红, 金芝, 张民.

    基于环境建模的物联网系统TAP规则生成方法.

    软件学报. 2021, 32(4):934-952.  http://www.jos.org.cn/1000-9825/6224.htm

  31. Xingwu Guo, Wenjie Wan, Zhaodi Zhang, Fu Song, Xuejun Wen, Min Zhang*: 

    Eager Falsification For Accelerating Robustness Verification of Deep Neural Networks. 

    The 32nd ISSRE, pp. 345-356, IEEE (CCF-B, 258700a345.pdf)

  32. Yiwei Zhu, Feng Wang, Wenjie Wan, Min Zhang*:

    Attack-Guided Efficient Robustness Verification of ReLU Neural Networks,

    The IJCNN, pp. 1-8, IEEE (CCF-C, IJCNN2021-YWZ.pdf)

  33. Zhaosen Wen, Min Zhang* and Weikai Miao:

    Fine-Grained Neural Network Abstraction for Efficient Formal Verification, 

    33rd SEKE, pp. 144-149, 2021. (CCF-C, paper071.pdf)

    34. 2020:

  34. Yi Wang, Min Zhang*: 

    Reducing implicit gender biases in software development: does intergroup contact theory work?, 

    The 28th EFEC/FSE, 580-592, ACM, 2020. (CCF-A, Distinguished Paper Award Nominee)

  35. Ming Hu, WenxueDuan, Min Zhang, Tongquan Wei, Mingsong Chen: 

    Quantitative Timing Analysis for Cyber-Physical Systems Using Uncertainty-Aware Scenario-Based Specifications. 

    IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11): 4006-4017, 2020 (CCF-A)

  36. Fei Gao, Frederic Mallet, Min Zhang*, Mingsong Chen: 

    Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint. 

    Design, Automation and Test in Europe (DATE 2020), pp. 376-381, IEEE (CCF-B)

  37. Dongdong An, Jing Liu, Min Zhang, Xiaohong Chen, Mingsong Chen, Haiying Sun. 

    Uncertainty modeling and runtime verification for autonomous vehicles driving control: A machine learning-based approach, 

    Journal of Software System, Vol. 167, 2020 （ SCI二区）

    38. 2019:

  38. Xiaohong Chen, Zhiwei Zhong, Zhi Jin, Min Zhang*, Tong Li, Xiang Chen and Tingliang Zhou: 

    Automating Consistency Verification of Safety Requirements for Railway Interlocking Systems. 

    The 27th RE, IEEE CSP, 2019 (CCF-B, Best Paper Award Nominee)

  39. Xiaotong Chi, Min Zhang*, Xiao Xu: 

    An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems. 

    The 26th APSEC, (CCF-C, Best Paper Award)

  40. Xiaoran Zhu, Min Zhang*, Jian Guo, Xin Li, Huibiao Zhu, Jifeng He: 

    Towards a unified executable formal automobile OS kernel and its applications.

    IEEE Transactions on Reliability, Vol. 68, No. 3, pp. 1117-1133, 2019. (pdf, SCI二区)

  41. Si Liu, Peter Ölveczky, Min Zhang*, Qi Wang and Jose Meseguer: 

    Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude.

    The 25th TACAS, ETAPS 2019, pp. 40-57, LNCS, Springer, 2019 (CCF-B) 

  42. Min Zhang, Fu Song, Frederic Mallet, Xiaohong Chen: 

    SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. 

    The 22nd FASE, ETAPS 2019, pp. 61-78, LNCS, Springer, 2019 (CCF-B) 

  43. Jiaqi Qian, Min Zhang*, Yi Wang, Kazuhiro Ogata: 

    KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. 

    The 22nd FASE, ETAPS 2019, pp. 229-305, LNCS, Springer, 2019 (CCF-B) 

  44. Ming Hu, Tongquan Wei, Min Zhang, Frederic Mallet, Mingsong Chen: 

    Sample-Guided Automated Synthesis for  CCSL Specifications. 

    The 56th DAC, IEEE CSP, 2019 （CCF-A)

    45. 2018:

  45. Min Zhang, Ogata Kazuhiro: 

    From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories. 

    Theoretical Computer Science , Vol. 722, pp. 52-75, Elsevier, 2018. (link, CCF-B)

  46. Min Zhang, Feng Dai, Frédéric Mallet: 

    Periodic scheduling for MARTE/CCSL: Theory and practice. 

    Science of Computer Programming, Vol. 154, pp. 42-60, Elsevier, 2018. (PDF, CCF-B)

  47. Yunhui Ying, Min Zhang*: 

    SMT-Based Approach to Formal Analysis of CCSL with Tool Support. 

    Ruan Jian Xue Bao/Journal of Software, Vol. 29(6), pp. 1-12, 2018. (in Chinese). (PDF, 中文)

  48. Frederic Mallet, Min Zhang*:  

    Work-in-Progress: From Logical Time Scheduling to Real-Time Scheduling. 

    39th RTSS, pp. 143-146, IEEE CSP, 2018 (CCF-A) 

  49. Wei Tang, Min Zhang*: 

    PyReload: Dynamic Updating of Python Programs by Reloading.

    25th APSEC, pp. 229-238, IEEE CSP, 2018 (CCF-C) 

  50. Feng Wang, Fu Song, Min Zhang, Xiaoran Zhu and Jun Zhang: 

    KRust: A Formal Executable Semantics of Rust. 

    12th TASE, pp. 44-51, IEEE CSP, 2018 (CCF-C)

  51. Wanling Xie, Huibiao Zhu, Min Zhang, Gang Lu, Yucheng Fang: 

    Formalization and Verification of Mobile Systems Calculus Using the Rewriting Engine Maude. 

    42nd COMPSAC, pp. 213-218, IEEE CSP, 2018 (CCF-C)

    52. 2017:

  52. Min Zhang, Yunhui Ying: 

    Towards SMT-based LTL Model Checking of Clock Constraint Specification Language for Real-Time and Embedded Systems (PDF)

    The 18th LCTES 2017, pp. 61-70, ACM, 2017. (CCF-B)

  53. Yuxin Deng, Min Zhang*, Guoqing Lei: 

    An Algebraic Approach to Automatic Reasoning for NetKAT based on its Operational Semantics. 

    The 19th ICFEM, pp. 464-480, LNCS, Springer-Verlag, 2017 (PDF, CCF-C).

  54. Jia She, Xiaoran Zhu, Min Zhang*: 

    Algebraic Formalization and Verification of PKMv3 Protocol using Maude
    The 29th SEKE, pp. 167-172,  2017, PDF, CCF-C) 

    55. 2016:

  55. Min Zhang, Toshiaki Aoki, Yueying He: 

    A spiral process of formalization and verification: a case study on verification of the scheduling mechanism of OSEK/VDX.  

    The Journal of Information Security and its Applications (JISA), Vol. 31, pp. 41-53, Elsevier, 2016. (PDF, CCF-C)

  56. Kazuhiro Ogata, Thapana Caimanont, and Min Zhang:  

    Formal Modeling and Analysis of Time- and Resource-sensitive Simple Business Processes.

    The Journal of Information Security and its Applications (JISA), Vol. 31, pp. 23-40, Elsevier, 2016.  (PDF, CCF-C)

  57. Min Zhang, Frédéric Mallet and Huibiao Zhu:  

    An SMT-based Approach to the Formal Analysis of MARTE/CCSL, 
    18th ICFEM, LNCS, Vol. 10009, pp. 433-449, Springer-Verlag, 2016. (PDF, CCF-C)

    58. 2015:

  58. Min Zhang, and Frederic Mallet: 

    An Executable Semantics of Clock Constraint Specification Language and its Applications 
    The 4th FTSCS 2015, CCIS, Vol. 596, Springer, pp. 37-51, 2015 (PDF)

  59. Min Zhang, and Kazuhiro Ogata, and Kokichi Futatsugi:  

    Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates.  

    The 22nd APSEC 2015, pp. 159-166, IEEE CSP (PDF, CCF-C)

  60. Min Zhang, and Toshiaki Aoki:

    A Spiral Process of Modeling and Verifying the Scheduling Mechanism of OSEK/VDX in OTS/CafeOBJ Method.  

    The 2nd DCIT 2015, pp. 159-166, IEEE CSP 

  61. Dung Tuan Ho, Min Zhang, Kazuhiro Ogata: 

    Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programming. 

    The 25th ILP 2015, pp. 33-47, CEUR

  62. Kazuhiro Ogata, and Thapana Caimanont, and Min Zhang: 

    Formal Modeling and Analysis of Time- and Resource-sensitive Simple Business Processes. 

    The 2nd DCIT 2015, pp. 11-20, IEEE CSP (Best Paper Award)

  63. Ha Thi Thu Doan, Wenjie Zhang, Min Zhang, Kazuhiro Ogata:  

    Model Checking Chandy-Lamport Distributed Snapshot Algorithm Revisited,  

    The 2nd DCIT 2015, pp. 30-39, IEEE CSP, 2015

    64. 2014 and before:

  64. Yunja Choi, Min Zhang, and Kazuhiro Ogata: 
    Evaluation of Maude as a test generation engine for automotive operating systems
    The 21st APSEC 2014, IEEE CSP (CCF-C)

  65. Min Zhang, Yunja Choi, Kazuhiro Ogata
    A Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications
    10th WRLA, LNCS 8663, Springer, pp. 280-296, 2014 (Click here for details.)

  66. Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
    Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method
     Specification, Algebra and Software (SAS), LNCS 8373, pp.560-577, 2014 ( pdf )

  67. Min Zhang, and Kazuhiro Ogata, and Kokichi Futatsugi: 
    Formalization and Verification of Behavioral Correctness of Dynamic Software Updates
    Electronic Notes in Theoretical Computer Science, Vol. 294, pp.11-13,2013

  68. Min Zhang, Kazuhiro Ogata, and Masaki Nakamura. 
    Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support.
    Special section on formal methods, IEICE Transaction, Vol.E94-D(5), pp.976-988. 2011 (zip file, SCI).

  69. Daniel Gaina, Min Zhang, Yuki Chiba and Y. Arimoto
    Constructor-based Inductive Theorem Prover
    The 5th CALCO, LNCS 8089, pp. 328-333, Springer, 2013

  70. Kazuhiro Ogata and Min Zhang 
    A Divide & Conquer Approach to Model Checking of Liveness Properties 
    The 37th COMPSAC, IEEE CSP, (2013, CCF-C)

  71. Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi: 
    An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms 
    The 19th APSEC, pp.664-673, (2012, CCF-C) [pdf]

  72. Min Zhang, Kazuhiro Ogata: 
    Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules
    The 19th APSEC, pp. 551-556, (2012, CCF-C) [pdf]

  73. Min Zhang, Kazuhiro Ogata: 
    Facilitating the Transformation of State Machines from Equations into Rewrite Rules. (pre-proceedings)
    The 9th WRLA: 182-197 (2012)

  74. Min Zhang, Kazuhiro Ogata, and Masaki Nakamura. 
    Specification Translation of State Machines from Equational Theories into Rewrite Theories. 
    The 12th ICFEM, LNCS 6447, pp.678-693, Springer-Verlag, 2010 (zip file, CCF-C).

  75. Yi Wang, Min Zhang 
    Penalty policies in professional software development practice: a multi-method field study. 
     In: 32nd ICSE, ACM, pp.39-47, 2010

  76. Min Zhang, and Kazuhiro Ogata. 
    Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications (Extended Version). 
     JAIST Technical report. IS-RR-2010-002: 1-16, 2009 (    pdf).

  77. Min Zhang, and Kazuhiro Ogata. 
    Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications.
    The 9th QISC, IEEE, pp. 406-411, 2009. (zip file, CCF-C)

  78. Min Zhang, Z. Qi, X. Dong:
    Executable Specification of P Systems with Active Membranes and its Implementation.
    Journal of Shanghai Jiaotong University. Vol. 42(10), 2008.

荣誉及奖励

无