个人简历

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

研究领域

软件工程，软件的形式化建模与验证，程序语言设计与分析，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!""

近期论文

2020:
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) (to appear, 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:
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
25th 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)
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)
Xiaotong Chi, Min Zhang*, Xiao Xu:
An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems
26th APSEC, (to appear, CCF-C)
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: 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)
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
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
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
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, and Min Zhang:
Formal Modeling and Analysis of Time- and Resource-sensitive Simple Business Processes
2nd DCIT 2015, pp. 11-20, IEEE CSP
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 (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
5th CALCO, LNCS 8089, pp. 328-333, Springer, 2013
Kazuhiro Ogata and Min 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 in professional software development practice: a multi-method field study.
In: 32nd ICSE, ACM, pp.39-47, 2010 (CCF-A)
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.
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.
PC member of DATE 2021
Co-chair of AI&FM 2019
Co-chair of YR-FMAC 2018
PC member of TASE 2018
PC member of FACS 2018
Program chair of TASE 2017
Publicity chair, local organization chair of TASE 2016
PC member of 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