张民 职称： 副教授
直属机构： 软件工程学院
学科：





11 访问


相关教师




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

教育经历
2008.04-2011.09：日本北陆先端科学技术大学院大学（JAIST）信息科学，软件科学博士
2005.09-2008.03：上海交通大学，计算机科学与工程系，BASICS实验室，软件硕士
2001.09-2005.06：山东师范大学，计算机科学与技术，本科


工作经历
2014.11.01-至今：华东师范大学，副教授
2011.10-2014.10：日本北陆先端科学技术大学院大学，博士后研究员



个人简介
心有所信，方能行远！

社会兼职
PC member of DATE 2021
Co-chair of AI&FM 2019
Co-chair of YR-FMAC 2018
PC member ofTASE 2018
PC member ofFACS 2018
Program chair of TASE 2017
Publicity chair, local organization chair of TASE 2016
PC memberof TASE 2016,ICFEM 2016
IEEE, ACM Member
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


研究方向
软件工程，软件的形式化建模与验证，程序语言设计与分析，Maude, Rewriting Logic等.
Recently I'm also interested in formal verification of AI systems.
Welcome those highly self-motivated students to join our group！Undergraduate students are welcome as well!




开授课程


科研项目


学术成果

2021:
YitingWu,Min Zhang*:Tightening Robustness Verification of Convolutional Neural Networks with Fine-Grained Linear Approximation.In proc. of the 35thAAAI, 2021 (CCF-A, to appear).
2020:
Yi Wang, Min Zhang*:Reducing implicit gender biases in software development: does intergroup contact theory work?,In proc.of the 28th EFEC/FSE, 580-592, ACM, 2020. (CCF-A, best paper award nominee)
Ming Hu, WenxueDuan, Min Zhang, TongquanWei, MingsongChen: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)
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)
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 （CCF-B, SCI二区）
2019:
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.27th RE, IEEE CSP, 2019 (CCF-B,best paper award nominee)
Xiaotong Chi,Min Zhang*, Xiao Xu:An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems.In the proc. of the 26th APSEC,(CCF-C, Best paper award)
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二区)
Si Liu, Peter ?lveczky,Min Zhang*, Qi Wang and Jose Meseguer:Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In the Proc. of the25th TACAS, ETAPS 2019, pp. 40-57, LNCS, Springer, 2019 (CCF-B)
Min Zhang, Fu Song, Frederic Mallet, Xiaohong Chen:SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language.22nd FASE, ETAPS 2019, pp. 61-78, LNCS, Springer, 2019 (CCF-B)
Jiaqi Qian,Min Zhang*, Yi Wang, Kazuhiro Ogata:KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs.22nd FASE, ETAPS 2019, pp. 229-305, LNCS, Springer, 2019 (CCF-B)
Ming Hu, Tongquan Wei,Min Zhang, Frederic Mallet, Mingsong Chen:Sample-Guided Automated Synthesis for CCSL Specifications.56th DAC, IEEE CSP, 2019（CCF-A)
2018:
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)
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)
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,中文CCF-A)
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)
Wei Tang,Min Zhang*:PyReload:DynamicUpdatingofPythonProgramsbyReloading. 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 ConstraintSpecification Language for Real-Time and Embedded Systems (PDF)18th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2017) pp. 61-70, ACM, 2017. (CCF-B)
Yuxin Deng,Min Zhang*, Guoqing Lei:An Algebraic Approach to Automatic Reasoning for NetKAT based on its Operational Semantics.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
29thSEKE,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, andMin 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
4thFTSCS 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.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.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.25th ILP 2015, pp. 33-47, CEUR
Kazuhiro Ogata, and Thapana Caimanont, andMin Zhang:Formal Modeling and Analysis of Time- and Resource-sensitive Simple Business Processes.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,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
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 (Clickherefor 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
5th CALCO, LNCS 8089, pp. 328-333, Springer, 2013
Kazuhiro Ogata andMin Zhang
A Divide & Conquer Approach to Model Checking of Liveness Properties
37th COMPSAC, IEEE CSP, (2013, CCF-C)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi:
An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms
19th APSEC, pp.664-673, (2012, CCF-C) [pdf]
Min Zhang, Kazuhiro Ogata:
Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules
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)
9th WRLA: 182-197 (2012)
Min Zhang, Kazuhiro Ogata, and Masaki Nakamura.
Specification Translation of State Machines from Equational Theories into Rewrite Theories.
In: 12th ICFEM, LNCS 6447, pp.678-693, Springer-Verlag, 2010 (zip file, CCF-C).
Yi Wang,Min Zhang
Penalty policies inprofessionalsoftware development practice: a multi-method field study.
In: 32nd ICSE, ACM, pp.39-47, 2010 (CCF-A)
Min Zhang, and KazuhiroOgata.
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.
In: 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.




荣誉及奖励
NEWS:
【2020.12】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！
【2020.12】2020级硕士研究生吴旖婷同学的论文被人工智能顶级会议AAAI'21录用！
【2020.09】2016级硕士研究生高飞同学毕业论文入选华东师范大学信息学部优秀毕业论文！
【2020.05】2016级硕士研究生迟晓彤同学被评委上海市优秀毕业生！
【2020.05】2020年入选法国蔚蓝海岸大学“Senior Professor”外籍****访问项目。

【2020.03】ECNU-Inria Associated Team for FM4CPS project is granted. (ECNU-Inria FM4CPS联合团队获得Inria资助）
【2019.12】迟晓彤同学的论文“An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems” 获APSEC2019最佳论文奖。

【2019.11】2017级硕士研究生高飞同学的学术论文“Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint”被DATE2020会议接收。
【2019.07】2019年中法“蔡元培”交流合作项目获得国家留学基金委资助，中方负责人。
【2019.06】2019年入选法国蔚蓝海岸大学“Senior Professor”外籍****访问项目。
【2019.01】2016级硕士研究生钱佳琪同学被评为华东师范大学优秀毕业生。

【2019.01】2016级硕士研究生钱佳琪同学的学术论文“KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs”被FASE 2019接收。
【2018.11】2016级硕士研究生唐玮同学获得国家励志奖学金，祝贺唐玮。
【2018.08】2015级博士研究生朱晓冉同学的学术论文“Towards a unified executable formal automobile OS kernel andits applications.”被IEEE Transactions on Reliability国际期刊录用。

【2018.08】国家自然科学基金面上项目 “基于时钟约束建模语言CCSL的实时嵌入式系统形式化验证与分析” 2019.01.01~2022.12.31, 主持人。
【2018.08】实验室获批华为OPEN HIRP项目资助。
【2018.03】实验室2018年度中法“徐光启”项目--基于SMT技术的时钟约束描述语言的形式化验证与分析 获批，中方负责人.
【2017.11】2015级硕士研究生应云辉同学的学术论文“基于SMT的时钟约束语言CCSL的形式化分析方法与工具”被软件学报录用。
【2017.03】2015级硕士研究生应云辉同学的学术论文“Towards SMT-based LTL Model Checking of Clock ConstraintSpecification Language for Real-Time and Embedded Systems”被LCTES 2017会议接收。

【2017.03】2014级硕士研究生代风同学被评为“校优秀毕业生”，祝贺代风。
【2015.08】国家自然科学基金青年项目 “基于模型检测的高可靠性软件动态更新的设计与验证” 2016.01.01~2018.12.31, 主持人