Navigation

  • About
  • Resume
  • Research Fields
  • Enrollment and Training
  • Course
  • Scientific
  • Academic Achievements
  • Honor
头像

Min Zhang

Related to the teacher

About

  • Department: Software Engineering Institute
  • Gender: male
  • Post: 200062
  • Graduate School:
  • Degree: Ph.D
  • Academic Credentials: Full Professor
  • Tel:
  • Email: zhangmin@sei.ecnu.edu.cn
  • Office: B1117, Science Building
  • Address: Science Building, No. 3663, North Zhongshan Road, Putuo, Shanghai
  • PostCode: 200062
  • Fax:

Education

2008.04-2011.09: Japan Advanced Institute of Science and Technology (JAIST), Ph.D in Software Engineering 

2005.09-2008.03: Shanghai Jiao Tong University, M.S. in Software Theory 

2001.09-2005.06: Shandong Normal University, B.S. Computer Science 

WorkExperience

2021.01-present： East China Normal University，Software Engineering Institute，Full Professor

2014.11-2020.12：East China Normal University，Software Engineering Institute，Associate Professor 

2011.10-2014.10：Japan Advanced Institute of Science and Technology (JAIST), post-doc researcher


Resume

I’m a full professor at Software Engineering Institute. I obtained my Ph.D in Software Engineering, at Ogata Lab in Japan Advanced Institute of Science and Technology (JAIST) in 2011, and my Master at the BASICS Lab in Shanghai Jiaotong University in 2008.

My research interests include formal methods for safety-critical systems such as real-time systems, AI-empowered systems and blockchains. Our researches have been funded by several agencies such as National Science Foundation of China (NSFC), France Campus, Israel Science Foundation (ISF), China Scholarship Council (CSC), and Huawei. I have co-authored more than 70 publications including several at top-tier conferences and journals such as CAV, NeurIPS, AAAI, ASE, ISSTA, OOPSLA, RTSS, FSE, TCS.

Other Appointments

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

Research Fields

I and my research team are mainly working on formal methods for various computer systems such as real-time systems, AI-driven systems and blockchains. In particular, we are focused on the following directions:

1. modeling and verifying real-time systems in logical clocks. 

2. formal verification of neural networks and AI-enabled systems 

3. formal verification of blockchains including smart contracts and distributed protocols. 

Two post-doc positions are open unitl 2023.12.01. 

Our research lab is seeking self-motivated post-doc researchers and PhD students who have strong research intersts in both AI and FM. 

We will provide competitive salary and treatment. Please contact me for CV to the mail address. 

zhangmin@sei.ecnu.edu.cn


Last update: 2023.11.05


Enrollment and Training

CALL FOR PEOPLE (CFP)

I'm seeking highly self-motivated graduate students and post-doc researchers to join my group. Please send me your resume to zhangmin@sei.ecnu.edu.cn if you are interested in applying. 


Awards for Students:  

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

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

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

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

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

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

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

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

  9. [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)

  10. [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)

  11. [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)

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

  13. [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. 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Course

Scientific

Academic Achievements

[VMCAI'25]Junfeng Yang, Min Zhang, Xin Chen, Qin Li: Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training. VMCAI 2025, (to appear)
[CAV'24]Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong, Min Zhang: Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. CAV 2024, pp. 401-426, Springer, 2024 (CCF-A, PDF)
[CAV'24]Haoze Wu,  Omri Isac, ..., Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CAV 2024, pp. 249 - 264, Springer, 2024  (CCF-A, PDF)
[ISSTA'24]Zhiyi Xue, Liangguo Li, Senyue Tian, Xiaohong Chen, Pingping Li, Liangyu Chen, Tingting Jiang, Min Zhang: LLM4Fin: Fully Automating LLM-Powered Test Case Generation for  FinTech Software Acceptance Testing. The ISSTA 2024, pp. 1661-1673, ACM (CCF-A, PDF)
[AAAI'24] 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)
[ICSE'24] 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, Research Track)
[ICSE'24] 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)
[VMCAI'24] 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)
[FAoC'24] Yuanrui Zhang, Frederic Mallet, Min Zhang, Zhiming LiuMin ZhangSpecification and Verification of Multi-clock Systems using a Temporal Logic with Clock ConstraintsFormal Aspects of Computing, Volume 36 Issue 2, 2024, (CCF-B, Link)
[TITS'24] Xiaohong Chen, Zhi Jin, Min Zhang, Frédéric Mallet, Xiaoshan Liu, Tingliang ZhouA Scalable Approach to Detecting SafetyRequirements Inconsistencies for Railway SystemsIEEE Transactions on Intelligent Transportation Systems (link)
[IoTJ'24] Liangyu Chen, Chen Wang, Cheng Chen, Caidie Huang, Xiaohong Chen, Min ZhangHomeGuard: A Lightweight SMT-Based Conflict Analysis for Trigger-Action ProgrammingIEEE Internet of Things (IoT) Journal, 2024 (Link)
[NeurIPS'23] Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Cheng Chen, Min Zhang:Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural NetworksThe 37th NeurIPS, 2023,  Accepted (CCF-A, Link)
[ISSTA'23] Zhiyi Xue, Si Liu, Zhaodi Zhang, Yiting Wu, Min Zhang:A Tale of Two Approximations: Tightening Over-Approximation for  DNN Robustness Verification via Under-ApproximationThe 32nd ISSTA, 2023, pp. 1182-1194, ACM. (CCF-A, Link)
[CVPR'23] Zhaodi Zhang, Zhiyi Xue, Yang Chen, Si Liu, Yueling Zhang, Jing Liu, Min Zhang:Boosting Verified Training for Robust Image Classifications via AbstractionThe CVPR, 2023 pp. 16251-16260,  (CCF-A, Link)
[TITS'23] 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 RequirementsThe IEEE Transactions on Intelligent Transportation Systems, 2023 (JCR Q1)
[TCAD'23] Ming Hu, Jun Xia, Min Zhang, Xiaohong Chen, Frederic Mallet, Mingsong Chen:Automated Synthesis of Safe Timing Behaviors for Requirements Models using CCSLThe IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023 (CCF-A, link)
[TCAD'23] Ming Hu, E Cao, Hongbing Huang, Min Zhang, Xiaohong Chen, Mingsong Chen:AIoTML: A Unified Modeling Language for AIoT-Based Cyber-Physical SystemsThe IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023 (CCF-A, link)
[TACAS'23] Xingwu Guo, Ziwei Zhou,  Yueling Zhang, Katz Guy, Min Zhang:OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural NetworksThe 29th TACAS, pp. 208-226, LNCS, Springer, 2023  (CCF-B, Link)
[AAAI'23] Xinping Wang, Liangyu Chen, Min Zhang:Deep Attentive Model for Knowledge Tracing    The 37th AAAI, pp. 10192-10199, AAAI, 2023 (CCF-A, Link)
[SETTA'22] 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)
[ASE'22] 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)
[ASE'22] 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)
[CAV'22] 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)
[OOPSLA'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)
[ToC'22] 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, 2022. (CCF-A, URL)
[FMCAD'22] Omri Isac, Clark Barrett, Min Zhang, Guy Katz : Neural Network Verification with Proof Production.FMCAD 2022, IEEE. (CCF-C, PDF)
[CompJ'22] Zhaodi Zhang, Jing Liu, Min Zhang, Haiying Sun: Efficient Robustness Verification of the Neural Networks in Smart IoT Devices.The Computer Journal. 2022 (CCF-B, PDF)
[SEKE'22] 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)
[AAAI'21] 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).
[SciDig'21] 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
[RTSS'21]  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)
[JoS'21] 边寒, 陈小红, 金芝, 张民.基于环境建模的物联网系统TAP规则生成方法. 软件学报. 2021, 32(4):934-952.  http://www.jos.org.cn/1000-9825/6224.htm
[ISSRE'21] 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)
[IJCNN'21] 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)
[SEKE'21] 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)
[FSE'20] 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)
[TCAD'20] 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)
[DATE'20] 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)
[JSS'20] 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二区）
[RE'19] 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)
[APSEC'19] 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)
[TRel'19] 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二区)
[TACAS'19] 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) 
[FASE'19] 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) 
[FASE'19] 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) 
[DAC'19] 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)
[TCS'19] 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)
[SCP'19] 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)
[JoS'18] 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, 中文)
[RTSS'18] 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) 
[APSEC'18] Wei Tang, Min Zhang*: PyReload: Dynamic Updating of Python Programs by Reloading. 25th APSEC, pp. 229-238, IEEE CSP, 2018 (CCF-C) 
[TASE'18] 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)
[COMPSAC'18] 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)
[LCTES'17] 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)
[ICFEM'17] 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).
[SEKE'17] Jia She, Xiaoran Zhu, Min Zhang*: Algebraic Formalization and Verification of PKMv3 Protocol using MaudeThe 29th SEKE, pp. 167-172,  2017, PDF, CCF-C) 
[JISA'16] 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)
[JISA'16] 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)
[ICFEM'16] 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)
[FTSCS'15] 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)
[APSEC'15] 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)
[APSEC'15] 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 
[ILP'15] 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
[DCIT'15] 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)
[DCIT'15] 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
[APSEC'14] Yunja Choi, Min Zhang, and Kazuhiro Ogata: Evaluation of Maude as a test generation engine for automotive operating systemsThe 21st APSEC 2014, IEEE CSP (CCF-C)
[WRLA'14] Min Zhang, Yunja Choi, Kazuhiro OgataA Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications10th WRLA, LNCS 8663, Springer, pp. 280-296, 2014 (Click here for details.)
[SAS'14] Min Zhang, Kazuhiro Ogata, Kokichi FutatsugiVerifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method Specification, Algebra and Software (SAS), LNCS 8373, pp.560-577, 2014 ( pdf )
[ENTCS'13] Min Zhang, and Kazuhiro Ogata, and Kokichi Futatsugi: Formalization and Verification of Behavioral Correctness of Dynamic Software UpdatesElectronic Notes in Theoretical Computer Science, Vol. 294, pp.11-13,2013
[IEICE'11] 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).
[CALCO'13] Daniel Gaina, Min Zhang, Yuki Chiba and Y. ArimotoConstructor-based Inductive Theorem ProverThe 5th CALCO, LNCS 8089, pp. 328-333, Springer, 2013
[COMPSAC'13] Kazuhiro Ogata and Min Zhang A Divide & Conquer Approach to Model Checking of Liveness Properties The 37th COMPSAC, IEEE CSP, (2013, CCF-C)
[APSEC'12] 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]
[APSEC'12] Min Zhang, Kazuhiro Ogata: Invariant-preserved Transformation of State Machines from Equations into Rewrite RulesThe 19th APSEC, pp. 551-556, (2012, CCF-C) [pdf]
[WRLA'12] Min Zhang, Kazuhiro Ogata: Facilitating the Transformation of State Machines from Equations into Rewrite Rules. (pre-proceedings)                    The 9th WRLA: 182-197 (2012)
[ICFEM'10] 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).
[ICSE'10] Yi Wang, Min Zhang Penalty policies in professional software development practice: a multi-method field study.  In: 32nd ICSE, ACM, pp.39-47, 2010
[TR'10] 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).
[QSIC'09] 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)
[JSJTU'08] 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.

Honor

PASSION IS THE BEST REWARD!