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.
Reviewers of the following journals and conferences:
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 tozhangmin@sei.ecnu.edu.cn if you are interested in applying.
Awards for Students:
[2023.10] 田家旭同学(M3)获得国家奖学金。
[2023.09] 田家旭(M3)、郅大鹏(D3)同学的论文“Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training ” 被第25届形式化方法国际权威会议VMCAI 2024(CCF-B类)录用。
[2023.09] 田家旭(M3)、郅大鹏(D3)同学的论文“Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural Networks”被第37届人工智能领域顶级会议NeurIPS 2023(CCF-A类)录用。
[2023.05] 薛志一(M2)、张兆迪(D4)、吴旖婷(M3)三位同学的论文A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation被ISSTA 2023(CCF-A类)录用。
[2023.02] 张兆迪(D4)、薛志一(M2)、陈洋(M2)三位同学的论文Boosting Verified Training for Robust Image Classifications via Abstraction被CVPR 2023(CCF-A类)录用。
[2022.12] 郭省吾(M2)、周孜为(B3)同学的论文OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks被国际顶级会议第29届TACAS 2023(CCF-B类)录用。
[2022.07] Our work 'Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks', has been acccepted by ASE 2022 (CCF-A)
[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)
[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)
[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)
[2022.05] 金鹏、田家旭、郅大鹏三位同学的论文Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning被形式化领域顶级会议CAV 2022(CCF-A类)录用!
[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.
[2021.08] 2021级硕士研究生郭省吾同学的论文Eager Falsification For Accelerating Robustness Verification of Deep Neural Networks被第32届国际软件过程可靠性会议ISSRE(CCF-B类)录用。
[2021.07] I will serve as TPC member for the Track D1 ofDATE 2022. Submit your contributions by Step. 12!
[2021.04] I will serve as PC member of FoMLAS 2021, a satellite workshop of CAV 2021!
[2020.12] I will co-chair TASE 2021 with Kazuhiro Ogata from 08/25 to 08/27 in 2021!
[2017.03] 2015级硕士研究生应云辉同学的学术论文“Towards SMT-based LTL Model Checking of Clock Constraint Specification Language for Real-Time and Embedded Systems”被LCTES 2017会议接收。
Periodic scheduling for MARTE/CCSL: Theory and practice.
Science of Computer Programming, Vol. 154, pp. 42-60, Elsevier, 2018. (PDF, )
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, 中文)
Frederic Mallet, Min Zhang*:
Work-in-Progress: From Logical Time Scheduling to Real-Time Scheduling.
39th RTSS, pp. 143-146, IEEE CSP, 2018 ()
Wei Tang, Min Zhang*:
PyReload: Dynamic Updating of Python Programs by Reloading.
25th APSEC, pp. 229-238, IEEE CSP, 2018 (CCF-C)
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)
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)
2017:
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. ()
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).
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)
2016:
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)
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)
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)
2015:
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)
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)
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
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
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)
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
2014 and before:
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)
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.)
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 )
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
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).
Daniel Gaina, Min Zhang, Yuki Chiba and Y. Arimoto Constructor-based Inductive Theorem Prover The 5th CALCO, LNCS 8089, pp. 328-333, Springer, 2013
Kazuhiro Ogata and Min Zhang A Divide & Conquer Approach to Model Checking of Liveness Properties The 37th COMPSAC, IEEE CSP, (2013, CCF-C)
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]
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]
Min Zhang, Kazuhiro Ogata: Facilitating the Transformation of State Machines from Equations into Rewrite Rules. (pre-proceedings) The 9th WRLA: 182-197 (2012)
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).
Yi Wang, Min Zhang Penalty policies in professional software development practice: a multi-method field study. In: 32nd ICSE, ACM, pp.39-47, 2010
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).
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)
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.