@book{zhou2017introduction,title={Introduction to Formal Semantics},author={Zhou, Chaochen and Zhan, Naijun},publisher={Academic Press (in Chinese)},year={2017},}
[B2]
Formal Verification of Simulink/Stateflow Diagrams
@book{zhan2016formal,title={Formal Verification of Simulink/Stateflow Diagrams},author={Zhan, Naijun and Wang, Shuling and Zhao, Hengjun},publisher={Springer-Verlag},year={2016},}
[B3]
MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems
Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, and Liang Zou
@incollection{chen2017mars,title={MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems},author={Chen, Mingshuai and Han, Xiao and Tang, Tao and Wang, Shuling and Yang, Mengfei and Zhan, Naijun and Zhao, Hengjun and Zou, Liang},booktitle={Provably Correct Systems, pp.39-58},year={2017},}
[B4]
Combining Formal and Informal Methods in the Design of Spacecrafts
Mengfei Yang and Naijun Zhan
In SETSS 2014, Lecture Notes in Computer Science 9506, Springer-Verlag. 2016, 2014
@incollection{yang2014combining,title={Combining Formal and Informal Methods in the Design of Spacecrafts},author={Yang, Mengfei and Zhan, Naijun},booktitle={SETSS 2014, Lecture Notes in Computer Science 9506, Springer-Verlag. 2016},year={2014},}
[B5]
Formal Modelling, Analysis and Verification of Hybrid Systems
Naijun Zhan, Shuling Wang, and Hengjun Zhao
In the Theories of Programming, Lecture Notes in Computer Science 8050, Springer-Verlag, 2013
@incollection{zhan2013formal,title={Formal Modelling, Analysis and Verification of Hybrid Systems},author={Zhan, Naijun and Wang, Shuling and Zhao, Hengjun},booktitle={the Theories of Programming, Lecture Notes in Computer Science 8050, Springer-Verlag},year={2013},}
Edited Volumes and Special Issues
[E1]
Formal Methods and Software Engineering - 26th International Conference on Formal Engineering Methods, ICFEM 2025
Étienne André, Jingyi Wang, and Naijun Zhan
Hangzhou, China, November 10-13, 2025, Proceedings. Lecture Notes in Computer Science 16229, Springer 2026, ISBN 978-981-95-4212-3, 2025
@misc{andr2025formal,title={Formal Methods and Software Engineering - 26th International Conference on Formal Engineering Methods, ICFEM 2025},author={André, Étienne and Wang, Jingyi and Zhan, Naijun},howpublished={Hangzhou, China, November 10-13, 2025, Proceedings. Lecture Notes in Computer Science 16229, Springer 2026, ISBN 978-981-95-4212-3},year={2025},}
[E2]
Formal Methods Syst. Des. 61(1)
Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan
@misc{huisman2023formal,title={Formal Methods Syst. Des. 61(1)},author={Huisman, Marieke and Pasareanu, Corina S. and Zhan, Naijun},howpublished={Special issue on FM 2021},year={2023},}
[E3]
Formal Aspects Comput. 35(2)
Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan
@misc{huisman2023formalb,title={Formal Aspects Comput. 35(2)},author={Huisman, Marieke and Pasareanu, Corina S. and Zhan, Naijun},howpublished={Special issue on FM 2021},year={2023},}
[E4]
Formal Methods - 24th International Symposium, FM 2021
Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan
Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0. (Editor), 2021
@misc{huisman2021formal,title={Formal Methods - 24th International Symposium, FM 2021},author={Huisman, Marieke and Pasareanu, Corina S. and Zhan, Naijun},howpublished={Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0. (Editor)},year={2021},}
[E5]
Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019
Partha S. Roop, Naijun Zhan, Sicun Gao, and Pierluigi Nuzzo
La Jolla, CA, USA, October 9-11, 2019. ACM 2019, ISBN 978-1-4503-6997-8. (Editor), 2019
@misc{roop2019proceedings,title={Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019},author={Roop, Partha S. and Zhan, Naijun and Gao, Sicun and Nuzzo, Pierluigi},howpublished={La Jolla, CA, USA, October 9-11, 2019. ACM 2019, ISBN 978-1-4503-6997-8. (Editor)},year={2019},}
[E6]
Symposium on Real-Time and Hybrid Systems
Cliff B. Jones, Ji Wang, and Naijun Zhan
Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday. Lecture Notes in Computer Science 11180, Springer 2018, ISBN 978-3-030-01460-5. (Editor), 2017
@misc{jones2017symposium,title={Symposium on Real-Time and Hybrid Systems},author={Jones, Cliff B. and Wang, Ji and Zhan, Naijun},howpublished={Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday. Lecture Notes in Computer Science 11180, Springer 2018, ISBN 978-3-030-01460-5. (Editor)},year={2017},}
[E7]
Dependable Software Engineering: Theories, Tools, and Applications
Martin Fränzle, Deepak Kapur, and Naijun Zhan
Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science 9984, ISBN 978-3-319-47676-6. (Editor), 2016
@misc{frnzle2016dependable,title={Dependable Software Engineering: Theories, Tools, and Applications},author={Fränzle, Martin and Kapur, Deepak and Zhan, Naijun},howpublished={Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science 9984, ISBN 978-3-319-47676-6. (Editor)},year={2016},}
[E8]
Formal Aspects Comput. 31(1)
Martin Fränzle, Deepak Kapur, Heike Wehrheim, and Naijun Zhan
@misc{frnzle2019formal,title={Formal Aspects Comput. 31(1)},author={Fränzle, Martin and Kapur, Deepak and Wehrheim, Heike and Zhan, Naijun},howpublished={Special issue on SETTA 2016},year={2019},}
@misc{easwaran2020journal,title={Journal of Systems Architecture},author={Easwaran, Arvind and Zhu, Qi and Zhan, Naijun},howpublished={Special issue on ICESS 2019},year={2020},}
[E10]
Journal of Software 27(3)
Naijun Zhan, Xuandong Li, and Ji Wang
Special issue on formal methods and its application. (in Chinese), 2016
@misc{zhan2016journal,title={Journal of Software 27(3)},author={Zhan, Naijun and Li, Xuandong and Wang, Ji},howpublished={Special issue on formal methods and its application. (in Chinese)},year={2016},}
Journal Papers
[J1]
MARS 2.0: A Toolchain for Designing Safety-Critical Cyber-Physical Systems
@article{TECS2026,title={MARS 2.0: A Toolchain for Designing Safety-Critical Cyber-Physical Systems},author={Xu, Xiong and Wang, Shuling and Zhan, Bohua and Mu, Binghao and Jin, Xiangyu and Lin, Guanhua and Li, Xing and Xu, Fanjiang and Gu, Bin and Yang, Mengfei and Zhan, Naijun},journal={To appear ACM TECS},year={2026}}
[J2]
Verified Numerical Semantics and Code Extraction for Simulink
@article{qi2026verified,title={Verified Numerical Semantics and Code Extraction for Simulink},author={Qi, Yuzhen and Wang, Shuling and Jin, Xiangyu and Xu, Xiong and Zhan, Naijun},journal={To appear IEEE TCAD (special issue of ESWEEK 2026)},year={2026},}
[J3]
Tolerant Barrier Certificates for Stochastic Systems
Shenghua Feng, Han Su, Hao Wu, Jie An, Mingshuai Chen, and Naijun Zhan
To appear IEEE TCAD (special issue of ESWEEK 2026), 2026
@article{feng2026tolerant,title={Tolerant Barrier Certificates for Stochastic Systems},author={Feng, Shenghua and Su, Han and Wu, Hao and An, Jie and Chen, Mingshuai and Zhan, Naijun},journal={To appear IEEE TCAD (special issue of ESWEEK 2026)},year={2026},}
[J4]
FAR-STL: Filter-Aware Robust Signal Temporal Logic for Online Monitoring of Cyber-Physical Systems
Supratim Gupta, Sobhan Chatterjee, Naijun Zhan, and Partha Roop
To appear IEEE TCAD (special issue of ESWEEK 2026), 2026
@article{gupta2026filter,title={FAR-STL: Filter-Aware Robust Signal Temporal Logic for Online Monitoring of Cyber-Physical Systems},author={Gupta, Supratim and Chatterjee, Sobhan and Zhan, Naijun and Roop, Partha},journal={To appear IEEE TCAD (special issue of ESWEEK 2026)},year={2026},}
[J5]
ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification
Yue Fang, Zhi Jin, Jie An, Jia Li, Hongshen Chen, Xiaohong Chen, and Naijun Zhan
@article{fang2026clarifystl,title={ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification},author={Fang, Yue and Jin, Zhi and An, Jie and Li, Jia and Chen, Hongshen and Chen, Xiaohong and Zhan, Naijun},journal={Accepted by ACM TOSEM},year={2026},}
[J6]
Path-sensitive abstract interpretation for WCET estimation
Shangshang Xiao, Mengxia Sun, Wei Zhhang, Naijun Zhan, and Lei Ju
@article{li2026termination,title={On Termination of Polynomial Programs with Equality Conditions},author={Li, Yangjia and Zhao, Liangran and Lu, Hui and Chen, Mingshuai and Wu, Guohua and Katoen, Joost-Pieter and Zhan, Naijun},journal={Information and Computation 312: 105487},year={2026},}
[J8]
Formal semantics for hierarchical Simulink diagrams in Isabelle/HOL
@article{qi2026formal,title={Formal semantics for hierarchical Simulink diagrams in Isabelle/HOL},author={Qi, Yuzhen and Wang, Shuling and Li, Xing and Zhan, Bohua and Zhan, Naijun},journal={Journal of Systems Architecture, 174: 103724},year={2026},}
[J9]
Piecewise Analysis of Probabilistic Programs via 𝑘-Induction
@article{yang2026piecewise,title={Piecewise Analysis of Probabilistic Programs via 𝑘-Induction},author={Yang, Tengshun and Feng, Shenghua and Fu, Hongfei and Zhan, Naijun and Ke, Jingyu and Wu, Shiyang},journal={Proc. ACM Program. Lang. 10 (POPL): 1933-1963},year={2026},}
@article{xu2025calculus,title={HpC: A Calculus for Hybrid and Mobile Systems},author={Xu, Xiong and Talpin, Jean-Pierre and Wang, Shuling and Wu, Hao and Zhan, Bohua and Liu, Xinxin and Zhan, Naijun},journal={Proc. ACM Program. Lang. 9 (OOPSLA1): 1158-1183 (2025)},year={2025},}
[J11]
Formal design of safety-critical systems with MARS
Yihao Yin, Hao Wu, Wan Liu, Shuling Wang, Xiong Xu, Wang Lin, Fanjiang Xu, and Naijun Zhan
@article{yin2026formal,title={Formal design of safety-critical systems with MARS},author={Yin, Yihao and Wu, Hao and Liu, Wan and Wang, Shuling and Xu, Xiong and Lin, Wang and Xu, Fanjiang and Zhan, Naijun},journal={Journal of Systems Architecture, 174:103711},year={2026},}
[J12]
A Brief History of Formal Methods in China
Naijun Zhan, Jim Woodcock, Ji Wang, and Mingshuai Chen
Accepted by Formal Aspects of Computing, in press, 2026
@article{zhan2026brief,title={A Brief History of Formal Methods in China},author={Zhan, Naijun and Woodcock, Jim and Wang, Ji and Chen, Mingshuai},journal={Accepted by Formal Aspects of Computing, in press},year={2026},}
[J13]
Modeling and Verification of Hybrid Systems by Extending AADL
@article{xu2025modeling,title={Modeling and Verification of Hybrid Systems by Extending AADL},author={Xu, Xiong and Ahmad, Ehsan and Wang, Shuling and Jin, Xiangyu and Zhan, Bohua and Zhan, Naijun},journal={ACM Transactions on Software Engineering and Methodology, 35(3):1-51},year={2025},}
[J14]
Active learning of deterministic timed automata via timed classification tree
Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang, Jie An, and Naijun Zhan
Science China Information Science, 68:222101, 2025
@article{teng2025active,title={Active learning of deterministic timed automata via timed classification tree},author={Teng, Yu and Chen, Hanyue and Mi, Junri and Zhang, Miaomiao and An, Jie and Zhan, Naijun},journal={Science China Information Science, 68:222101},year={2025},}
[J15]
WCET Estimation for CNN Inference on FPGA SoC with Multi-DPU Engines
Wei Zhang, Yunlong Yu, Xiao Jiang, Nan Guan, Naijun Zhan, and Lei Ju
IEEE Transactions on Parallel and Distributed Systems, 36(6):1146-1160, 2025
@article{zhang2025wcet,title={WCET Estimation for CNN Inference on FPGA SoC with Multi-DPU Engines},author={Zhang, Wei and Yu, Yunlong and Jiang, Xiao and Guan, Nan and Zhan, Naijun and Ju, Lei},journal={IEEE Transactions on Parallel and Distributed Systems, 36(6):1146-1160},year={2025},}
[J16]
Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, and Zhihong Yang
ACM Transactions on Programming Languages and Systems, 47(1):1-35, 2024
@article{wu2024synthesizing,title={Synthesizing Invariants for Polynomial Programs by Semidefinite Programming},author={Wu, Hao and Wang, Qiuye and Xue, Bai and Zhan, Naijun and Zhi, Lihong and Yang, Zhihong},journal={ACM Transactions on Programming Languages and Systems, 47(1):1-35},year={2024},}
[J17]
A Correct-by-Construction Way to the Design of CPS
Naijun Zhan, Han Su, Mengfei Yang, and Bin Gu
Research Direction: Cyber-Physical Systems, 2(e7):1-7, 2024
@article{zhan2024correct,title={A Correct-by-Construction Way to the Design of CPS},author={Zhan, Naijun and Su, Han and Yang, Mengfei and Gu, Bin},journal={Research Direction: Cyber-Physical Systems, 2(e7):1-7},year={2024},}
[J18]
Modelling and Analysis of the LatestTime Message Synchronization Policy in ROS
Chenhao Wu, Rruoxiang Li, Naijun Zhan, and Nan Guan
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(11): 3576-3587. (Special issue of EMSOFT 2024), 2024
@article{wu2024modelling,title={Modelling and Analysis of the LatestTime Message Synchronization Policy in ROS},author={Wu, Chenhao and Li, Rruoxiang and Zhan, Naijun and Guan, Nan},journal={IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(11): 3576-3587. (Special issue of EMSOFT 2024)},year={2024},}
[J19]
Reach-Avoid Analysis for Stochastic Differential Equations
Bai Xue, Naijun Zhan, and Martin Fränzle
IEEE Transactions on Automatic Control, 69(3): 1882-1889, 2023
@article{xue2023reach,title={Reach-Avoid Analysis for Stochastic Differential Equations},author={Xue, Bai and Zhan, Naijun and Fränzle, Martin},journal={IEEE Transactions on Automatic Control, 69(3): 1882-1889},year={2023},}
[J20]
Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints
@article{wu2024decision,title={Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints},author={Wu, Hao and Chen, Yu-Fang and Wu, Zhilin and Xia, Bican and Zhan, Naijun},journal={Acta Informatica, 61(1): 23-52},year={2024},}
[J21]
Reach-avoid Verification Based on Convex Optimization
Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, and Wanwei Liu
IEEE Transactions on Automatic Control, 69(1): 598-605, 2024
@article{xue2024reach,title={Reach-avoid Verification Based on Convex Optimization},author={Xue, Bai and Zhan, Naijun and Fränzle, Martin and Wang, Ji and Liu, Wanwei},journal={IEEE Transactions on Automatic Control, 69(1): 598-605},year={2024},}
[J22]
Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan
Proc. ACM Program. Lang., (OOPSLA), 7: 696-726, 2023
@article{feng2023lower,title={Lower Bounds for Possibly Divergent Probabilistic Programs},author={Feng, Shenghua and Chen, Mingshuai and Su, Han and Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Zhan, Naijun},journal={Proc. ACM Program. Lang., (OOPSLA), 7: 696-726},year={2023},}
[J23]
Encoding inductive invariants as barrier certificates synthesis via difference-of-convex programming
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen
Information and Computation 289:104965 (Extended version of CAV 2021 paper), 2022
@article{wang2022encoding,title={Encoding inductive invariants as barrier certificates synthesis via difference-of-convex programming},author={Wang, Qiuye and Chen, Mingshuai and Xue, Bai and Zhan, Naijun and Katoen, Joost-Pieter},journal={Information and Computation 289:104965 (Extended version of CAV 2021 paper)},year={2022},}
[J24]
A denotational semantics of Simulink with higher-order UTP
@article{xu2022denotational,title={A denotational semantics of Simulink with higher-order UTP},author={Xu, Xiong and Zhan, Bohua and Wang, Shuling and Talpin, Jean-Pierre and Zhan, Naijun},journal={Journal of Logical and Algebraic Methods in Programming, 130: 100809},year={2022},}
[J25]
Formal Analysis of 5G AKMA
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, and Bifei Mao
@article{yang2022formal,title={Formal Analysis of 5G AKMA},author={Yang, Tengshun and Wang, Shuling and Zhan, Bohua and Zhan, Naijun and Li, Jinghui and Xiang, Shuangqing and Xiang, Zhan and Mao, Bifei},journal={Journal of System Architecture, 126: 102478},year={2022},}
[J26]
Semantics foundation for cyber-physical systems using higher-order UTP
@article{xu2022semantics,title={Semantics foundation for cyber-physical systems using higher-order UTP},author={Xu, Xiong and Zhan, Bohua and Wang, Shuling and Talpin, Jean-Pierre and Zhan, Naijun},journal={ACM Transactions on Software Engineering and Methodology, 32(1), Article No. 9:1-48},year={2022},}
[J27]
Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow
@article{xu2021unified,title={Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow},author={Xu, Xiong and Zhan, Bohua and Wang, Shuling and Jin, Xiangyu and Talpin, Jean-Pierre and Zhan, Naijun},journal={Theoretical Computer Science, 903:1-25},year={2021},}
[J28]
Learning Nondeterministic Real-Time Automata
Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang
ACM Transaction on Embedded Computing Systems, Article 7:1-25, special issue of EMSOFT 2021, 20(5s) 99:1-99:26, 2021
@article{an2021learning,title={Learning Nondeterministic Real-Time Automata},author={An, Jie and Zhan, Bohua and Zhan, Naijun and Zhang, Miaomiao},journal={ACM Transaction on Embedded Computing Systems, Article 7:1-25, special issue of EMSOFT 2021, 20(5s) 99:1-99:26},year={2021},}
[J29]
Safety Guarantee for Time-Delay Systems with Disturbances by Control Barrier Functionals
Wenyou Liu, Yunjun Bai, Li Jiao, Bai Xue, and Naijun Zhan
Science China Information Science, 66: 132102, 2023
@article{liu2023safety,title={Safety Guarantee for Time-Delay Systems with Disturbances by Control Barrier Functionals},author={Liu, Wenyou and Bai, Yunjun and Jiao, Li and Xue, Bai and Zhan, Naijun},journal={Science China Information Science, 66: 132102},year={2023},}
[J30]
Inferring Nonlinear Switched Dynamical Systems
Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang
@article{jin2021inferring,title={Inferring Nonlinear Switched Dynamical Systems},author={Jin, Xiangyu and An, Jie and Zhan, Bohua and Zhan, Naijun and Zhang, Miaomiao},journal={Formal Aspects of Computing, 33(3): 385-406},year={2021},}
[J31]
Switching Controller Synthesis for Time-delayed Hybrid Systems
Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, and Naijun Zhan
Science China Mathematica, 51(1):97-114. (in Chinese), 2021
@article{bai2021switching,title={Switching Controller Synthesis for Time-delayed Hybrid Systems},author={Bai, Yunjun and Gan, Ting and Jiao, Li and Xia, Bican and Xue, Bai and Zhan, Naijun},journal={Science China Mathematica, 51(1):97-114. (in Chinese)},year={2021},}
[J32]
Synthesizing robust domains of attraction for state-constrained perturbed polynomial systems
Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, and Zhikun She
SIAM J. on Control and Optimization, 59(2): 1083-1108, 2021
@article{xue2021synthesizing,title={Synthesizing robust domains of attraction for state-constrained perturbed polynomial systems},author={Xue, Bai and Wang, Qiuye and Zhan, Naijun and Wang, Shijie and She, Zhikun},journal={SIAM J. on Control and Optimization, 59(2): 1083-1108},year={2021},}
[J33]
Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems
Bai Xue and Naijun Zhan
IEEE Transactions on Automatic Control, 67(2):1053-1060, 2022
@article{xue2022robust,title={Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems},author={Xue, Bai and Zhan, Naijun},journal={IEEE Transactions on Automatic Control, 67(2):1053-1060},year={2022},}
[J34]
Safety Verification for Random Ordinary Differential Equations
Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, and Bican Xia
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,39(11):4090-4101. (Special issue of EMSOFT 2020), 2020
@article{xue2020safety,title={Safety Verification for Random Ordinary Differential Equations},author={Xue, Bai and Fränzle, Martin and Zhan, Naijun and Bogomolov, Sergiy and Xia, Bican},journal={IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,39(11):4090-4101. (Special issue of EMSOFT 2020)},year={2020},}
[J35]
Indecision and delays are the parents of failure – Taming them algorithmically by synthesizing delay-resilient control
Mingshuai Chen, Martin Fraenzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan
@article{chen2020indecision,title={Indecision and delays are the parents of failure – Taming them algorithmically by synthesizing delay-resilient control},author={Chen, Mingshuai and Fraenzle, Martin and Li, Yangjia and Mosaad, Peter N. and Zhan, Naijun},journal={Acta Informatica, 58(5): 497-528},year={2020},}
[J36]
Over- and Under-Approximating Reach Sets for Perturbed Delay Differential Equations
Bai Xue, Qiuye Wang, Shenghua Feng, and Naijun Zhan
IEEE Transactions on Automatic Control, 66(1): 283-290, 2020
@article{xue2020over,title={Over- and Under-Approximating Reach Sets for Perturbed Delay Differential Equations},author={Xue, Bai and Wang, Qiuye and Feng, Shenghua and Zhan, Naijun},journal={IEEE Transactions on Automatic Control, 66(1): 283-290},year={2020},}
[J37]
Learning real-time automata
Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang
Science China Information Science, 64:192103:1–192103:17, 2020
@article{an2020learning,title={Learning real-time automata},author={An, Jie and Wang, Lingtai and Zhan, Bohua and Zhan, Naijun and Zhang, Miaomiao},journal={Science China Information Science, 64:192103:1–192103:17},year={2020},}
[J38]
From model to implementation: A network algorithm programming language
Jian Wang, Jie An, Mingshuai Cheng, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan
Science China Information Science, 63(7):172102:1–172102:17, 2020
@article{wang2020from,title={From model to implementation: A network algorithm programming language},author={Wang, Jian and An, Jie and Cheng, Mingshuai and Zhan, Naijun and Wang, Lulin and Zhang, Miaomiao and Gan, Ting},journal={Science China Information Science, 63(7):172102:1–172102:17},year={2020},}
[J39]
Automatically generating SystemC code from HCSP formal mdoels
Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, and Naijun Zhan
ACM Transactions on Software Engineering and Methodology, 29(1), Article 4:1-39. (Extended version of FM 2016 paper), 2020
@article{yan2020automatically,title={Automatically generating SystemC code from HCSP formal mdoels},author={Yan, Gaogao and Jiao, Li and Wang, Shuling and Wang, Lingtai and Zhan, Naijun},journal={ACM Transactions on Software Engineering and Methodology, 29(1), Article 4:1-39. (Extended version of FM 2016 paper)},year={2020},}
[J40]
Inner approximating reachable sets for polynomial systems with time-varying uncertainties
Bai Xue, Martin Fraenzle, and Naijun Zhan
IEEE Transactions on Automatic Control, 65(4):1468-1483, 2020
@article{xue2020inner,title={Inner approximating reachable sets for polynomial systems with time-varying uncertainties},author={Xue, Bai and Fraenzle, Martin and Zhan, Naijun},journal={IEEE Transactions on Automatic Control, 65(4):1468-1483},year={2020},}
[J41]
The opacity of real-time automata
Lingtai Wang, Naijun Zhan, and Jie An
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11): 2845-2856. (Special issue of EMSOFT 2018), 2018
@article{wang2018opacity,title={The opacity of real-time automata},author={Wang, Lingtai and Zhan, Naijun and An, Jie},journal={IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11): 2845-2856. (Special issue of EMSOFT 2018)},year={2018},}
[J42]
Reachability analysis for solvable dynamical systems
@article{gan2018reachability,title={Reachability analysis for solvable dynamical systems},author={Gan, Ting and Chen, Mingshuai and Li, Yangjia and Xia, Bican and Zhan, Naijun},journal={IEEE Transactions on Automatic Control, 63(7): 2003-2018},year={2018},}
[J43]
Generating semi-algebraic invariants for non-autonomous hybrid systems
Qiuye Wang, Yangjia Li, Bican Xia, and Naijun Zhan
Journal of System Science and Complexity, 30(1):234-253, 2017
@article{wang2017generating,title={Generating semi-algebraic invariants for non-autonomous hybrid systems},author={Wang, Qiuye and Li, Yangjia and Xia, Bican and Zhan, Naijun},journal={Journal of System Science and Complexity, 30(1):234-253},year={2017},}
[J44]
A compositional modelling and verification framework for stochastic hybrid systems
Shuling Wang, Naijun Zhan, and Lijun Zhang
Formal Aspects of Computing, 29(4):751-775. (extended version of SETTA 2015 paper), 2017
@article{wang2017compositional,title={A compositional modelling and verification framework for stochastic hybrid systems},author={Wang, Shuling and Zhan, Naijun and Zhang, Lijun},journal={Formal Aspects of Computing, 29(4):751-775. (extended version of SETTA 2015 paper)},year={2017},}
[J45]
Modelling and Verifying Communication Failure of Hybrid Systems in HCSP
Shuling Wang, Flemming Nielson, Hanne Riis Nielson, and Naijun Zhan
@article{wang2017modelling,title={Modelling and Verifying Communication Failure of Hybrid Systems in HCSP},author={Wang, Shuling and Nielson, Flemming and Nielson, Hanne Riis and Zhan, Naijun},journal={Computer Journal, 60(8):1111-1130},year={2017},}
@article{dai2017barrier,title={Barrier certificate revisited},author={Dai, Liyun and Gan, Ting and Xia, Bican and Zhan, Naijun},journal={Journal of Symbolic Computation, 80:62-86},year={2017},}
[J47]
Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL
Ehsan Ahmad, Yunwei Dong, Brian Larsen, Jidong Lv, Tao Tang, and Naijun Zhan
Science China Information Sciences, 58(11):1-20, 2015
@article{ahmad2015behavior,title={Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL},author={Ahmad, Ehsan and Dong, Yunwei and Larsen, Brian and Lv, Jidong and Tang, Tao and Zhan, Naijun},journal={Science China Information Sciences, 58(11):1-20},year={2015},}
[J48]
Formal anlysis and verification of Chinese Train Control System
Danqing Guo, Jidong Lv, Shuling Wang, Tao Tang, Naijun Zhan, Datian Zhou, and Liang Zou
Science China Information Sciences, 45(3):417-438 (in Chinese), 2015
@article{guo2015formal,title={Formal anlysis and verification of Chinese Train Control System},author={Guo, Danqing and Lv, Jidong and Wang, Shuling and Tang, Tao and Zhan, Naijun and Zhou, Datian and Zou, Liang},journal={Science China Information Sciences, 45(3):417-438 (in Chinese)},year={2015},}
[J49]
Discovering non-terminating inputs for polynomial programs
Jiang Liu, Ming Xu, Naijun Zhan, and Hengjun Zhao
Journal of System Science and Complexity, 27(6):1286-1304, 2014
@article{liu2014discovering,title={Discovering non-terminating inputs for polynomial programs},author={Liu, Jiang and Xu, Ming and Zhan, Naijun and Zhao, Hengjun},journal={Journal of System Science and Complexity, 27(6):1286-1304},year={2014},}
[J50]
Model-checking Conditional CSL for Continuous-time Markov Chains
Yang Gao, Ming Xu, Naijun Zhan, and Lijun Zhang
Information Processing Letters, 113(1-2):44-50, 2013
@article{gao2013model,title={Model-checking Conditional CSL for Continuous-time Markov Chains},author={Gao, Yang and Xu, Ming and Zhan, Naijun and Zhang, Lijun},journal={Information Processing Letters, 113(1-2):44-50},year={2013},}
[J51]
Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
Jiang Liu, Naijun Zhan, and Hengjun Zhao
Mathematics in Computer Science, 6:395-408, 2012, 2012
@article{xia2011symbolic,title={Symbolic decision procedure for termination},author={Xia, Bican and Yang, Lu and Zhan, Naijun and Zhang, Zhihai},journal={Formal Aspects of Computing, 23(2):171-190, 2011. DOI: 10.1007/s00165-009-0144-5},year={2011},}
[J53]
Rate Monotonic Scheduling Re-analyzed
Qiwen Xu and Naijun Zhan
Information Processing Letters, 110(6): 226-231. DOI: 10.1016/j.ipl.2009.12.010, 2010
@article{zhan2010connection,title={Connection between algebraical and logical approaches to concurrent systems},author={Zhan, Naijun},journal={Mathematical Structures in Computer Science, 20(5):915-950},year={2010},}
[J55]
Recent advances in program verification through computer algebra
Yang Lu, Chaochen Zhou, Naijun Zhan, and Bican Xia
Frontiers of Computer Science in China, 4(1):1-16, 2010
@article{lu2010recent,title={Recent advances in program verification through computer algebra},author={Lu, Yang and Zhou, Chaochen and Zhan, Naijun and Xia, Bican},journal={Frontiers of Computer Science in China, 4(1):1-16},year={2010},}
[J56]
On hierarchically developing reactive systems
Naijun Zhan and Mila Majster-Cederbaum
Information and Computation, 208(9):997-1019, 2010
@article{chen2009refinement,title={Refinement and verification in component based and model driven design},author={Chen, Zhenbang and Liu, Zhiming and Stolz, Volker and Ravn, Anders P. and Zhan, Naijun},journal={Science of Computer Programming, 74(4):168-196},year={2009},}
[J58]
Formalizing scheduling theorems using duration calculus
@article{qiwen2008formalizing,title={Formalizing scheduling theorems using duration calculus},author={Qiwen, Xu and Zhan, Naijun},journal={Nordic Journal of Computing, 14:173- 201},year={2008},}
[J59]
Basic research in computer science and software engineering at SKLCS
@article{zhang2008basic,title={Basic research in computer science and software engineering at SKLCS},author={Zhang, Jian and Zhang, Wenhui and Zhan, Naijun and Shen, Yidong and Chen, Haiming and Zhang, Yunquan and Wang, Yongji and Wu, Enhua and Wang, Hongan and Zhu, Xueyang},journal={Frontiers of Computer Science in China, 2(1): 1-11},year={2008}}
[J60]
Compositional properties of sequential processes
Naijun Zhan
Electronic Notes in Theoretical Computer Science, 118:111-128, 2004
@article{zhan2001intuitive,title={An intuitive proof for DDS},author={Zhan, Naijun},journal={Journal of Computer Science and Technology, 16(2):146-158},year={2001}}
@inproceedings{Zhu2026PDE,title={PAC Verification of STL for Linear Parabolic PDEs },author={Zhu, Jiyu and Feng, Shenghua and An, Jie and Zhan, Naijun},booktitle={EMSOFT 2026 (to appear, WiP)},year={2026},}
[C2]
Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees
@inproceedings{chi2026synthesizing,title={Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees},author={Chi, Zhiming and Zhao, Lutan and Liu, Depeng and Li, Yong and Yang, Pengfei and Wang, Bow-Yaw and ui Hou and heng-Chao Huang and Turrini, Adrea and Zhang, Lijun and Zhan, Naijun},booktitle={ATVA 2026 (to appear)},year={2026},}
[C3]
TiMoE: Timing-Predictable Inference System for MoE Large Language Models
Shangshang Xiao, Wei Zhang, Yongxin Jiao, Fajun Xv, Naijun Zhan, and Lei Ju
@inproceedings{xiao2026timoe,title={TiMoE: Timing-Predictable Inference System for MoE Large Language Models},author={Xiao, Shangshang and Zhang, Wei and Jiao, Yongxin and Xv, Fajun and Zhan, Naijun and Ju, Lei},booktitle={RTSS 2026 (to appear)},year={2026}}
[C4]
Mining DTA with SMT by Exploiting Simple Elementary Language
@inproceedings{wang2026mining,title={Mining DTA with SMT by Exploiting Simple Elementary Language},author={Wang, Ziran and An, Jie and Zhan, Naijun},booktitle={RTSS 2026 (to appear)},year={2026}}
[C5]
Verified Numerical Semantics and Code Extraction for Simulink
@inproceedings{qi2026verifiedb,title={Verified Numerical Semantics and Code Extraction for Simulink},author={Qi, Yuzhen and Wang, Shuling and Jin, Xiangyu and Xu, Xiong and Zhan, Naijun},booktitle={EMSOFT 2026, to appear IEEE TCAD},year={2026},}
[C6]
Tolerant Barrier Certificates for Stochastic Systems
Shenghua Feng, Han Su, Hao Wu, Jie An, Mingshuai Chen, and Naijun Zhan
@inproceedings{feng2026tolerantb,title={Tolerant Barrier Certificates for Stochastic Systems},author={Feng, Shenghua and Su, Han and Wu, Hao and An, Jie and Chen, Mingshuai and Zhan, Naijun},booktitle={EMSOFT 2026, to appear IEEE TCAD},year={2026},}
[C7]
FAR-STL: Filter-Aware Robust Signal Temporal Logic for Online Monitoring of Cyber-Physical Systems
Supratim Gupta, Sobhan Chatterjee, Naijun Zhan, and Partha Roop
@inproceedings{gupta2026filterb,title={FAR-STL: Filter-Aware Robust Signal Temporal Logic for Online Monitoring of Cyber-Physical Systems},author={Gupta, Supratim and Chatterjee, Sobhan and Zhan, Naijun and Roop, Partha},booktitle={EMSOFT 2026, to appear IEEE TCAD},year={2026},}
[C8]
PRM-PBE: Process Reward Model for Reinforcement Learning in Programming-by-Example
Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Jiangmeng Li, Xiaohong Chen, and Naijun Zhan
@inproceedings{fang2026process,title={PRM-PBE: Process Reward Model for Reinforcement Learning in Programming-by-Example},author={Fang, Yue and Jin, Zhi and An, Jie and Chen, Hongshen and Li, Jiangmeng and Chen, Xiaohong and Zhan, Naijun},booktitle={the Proceedings of ICML 2026},year={2026},}
[C9]
How Powerful are LLMs in Generating Program Specifications
Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan, and Fanjiang Xu
@inproceedings{yang2026powerful,title={How Powerful are LLMs in Generating Program Specifications},author={Yang, Fanpeng and Li, Xing and Wang, Shuling and An, Jie and Sun, Zeyu and Feng, Shenghua and Wang, Wenhan and Wang, Weiyi and Zhan, Naijun and Xu, Fanjiang},booktitle={? In the Proceedings of ICML 2026},year={2026},}
[C10]
A complete proof system for HyperLTL
Naijun Zhan, Wen Tang, and Dimitar Guelev
In Proceedings of IJCAR 2026, Lecture Notes in Computer Science 16688, pp.377-395, 2026
@inproceedings{zhan2026complete,title={A complete proof system for HyperLTL},author={Zhan, Naijun and Tang, Wen and Guelev, Dimitar},booktitle={Proceedings of IJCAR 2026, Lecture Notes in Computer Science 16688, pp.377-395},year={2026},}
[C11]
Path-sensitive abstract interpretation for WCET estimation
Shangshang Xiao, Mengxia Sun, Wei Zhhang, Naijun Zhan, and Lei Ju
In the Proceedings of PLDI 2026, Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 174, 2026
@inproceedings{xiao2026pathb,title={Path-sensitive abstract interpretation for WCET estimation},author={Xiao, Shangshang and Sun, Mengxia and Zhhang, Wei and Zhan, Naijun and Ju, Lei},booktitle={the Proceedings of PLDI 2026, Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 174},year={2026},}
[C12]
Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
@inproceedings{zhao2026formal,title={Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel},author={Zhao, Tianqi and Cao, Qinxiang and Feng, Shenghua and Zhou, Minghui and Zhan, Naijun and Cao, Yongzhi and Zhao, Junfeng and Zhao, Haiyan and Wang, Hao and Hu, Zhenjiang},booktitle={the Proceedings of FM 2026, Lecture Notes in Computer Science 16557, pp.651-669},year={2026},}
[C13]
Exact Moment Estimation of Stochastic Differential Dynamics
Shenghua Feng, Jie An, Naijun Zhan, and Fanjiang Xu
In the Proceedings of FM 2026, Lecture Notes in Computer Science 16557, pp.71-89, 2026
@inproceedings{feng2026exact,title={Exact Moment Estimation of Stochastic Differential Dynamics},author={Feng, Shenghua and An, Jie and Zhan, Naijun and Xu, Fanjiang},booktitle={the Proceedings of FM 2026, Lecture Notes in Computer Science 16557, pp.71-89},year={2026},}
[C14]
Derivative-Agnostic Inference of Nonlinear Hybrid Systems
Hengzhi Yu, Bohan Ma, Mingshuai Chen, Huangying Dong, Jie An, Bin Gu, Naijun Zhan, and Jianwei Yin
In the Proceedings of HSCC/ICCPS 2026 (to appear), 2026
@inproceedings{yu2026derivative,title={Derivative-Agnostic Inference of Nonlinear Hybrid Systems},author={Yu, Hengzhi and Ma, Bohan and Chen, Mingshuai and Dong, Huangying and An, Jie and Gu, Bin and Zhan, Naijun and Yin, Jianwei},booktitle={the Proceedings of HSCC/ICCPS 2026 (to appear)},year={2026},}
[C15]
Quantifier Elimination Meets Treewidth
Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, and Naijun Zhan
In the Proceedings of TACAS 2026, Lecture Notes in Computer Science 16505, pp.353-373, 2026
@inproceedings{wu2026quantifier,title={Quantifier Elimination Meets Treewidth},author={Wu, Hao and Zhu, Jiyu and Goharshady, Amir Kafshdar and An, Jie and Xia, Bican and Zhan, Naijun},booktitle={the Proceedings of TACAS 2026, Lecture Notes in Computer Science 16505, pp.353-373},year={2026},}
[C16]
RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation
Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen, and Naijun Zhan
@inproceedings{fang2026restl,title={RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation},author={Fang, Yue and Jin, Zhi and An, Jie and Chen, Hongshen and Chen, Xiaohong and Zhan, Naijun},booktitle={the Proc. of AAAI 2026, pp.30682-30689},year={2026},}
[C17]
Piecewise Analysis of Probabilistic Programs via 𝑘-Induction
@inproceedings{yang2026piecewiseb,title={Piecewise Analysis of Probabilistic Programs via 𝑘-Induction},author={Yang, Tengshun and Feng, Shenghua and Fu, Hongfei and Zhan, Naijun and Ke, Jingyu and Wu, Shiyang},booktitle={the Proceedings of POPL 2026},year={2026},}
[C18]
On Synthesis of Timed Regular Expressions
Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, and Zhenya Zhang
@inproceedings{wang2025synthesis,title={On Synthesis of Timed Regular Expressions},author={Wang, Ziran and An, Jie and Zhan, Naijun and Zhang, Miaomiao and Zhang, Zhenya},booktitle={the Proceedings of RTSS 2025, pp.311-323},year={2025},}
[C19]
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang, and Naijun Zhan
In the Proc. of SETTA 2025, Lecture Notes in Computer Science 16458, pp.113-133, 2025
@inproceedings{jin2025hhlpar,title={HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes},author={Jin, Xiangyu and Zhan, Bohua and Wang, Shuling and Zhan, Naijun},booktitle={the Proc. of SETTA 2025, Lecture Notes in Computer Science 16458, pp.113-133},year={2025},}
[C20]
Efficient Decomposition Identification of Deterministic Finite Automata from Examples
Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu Naijun Zhan, and Miaomiao Zhang
In the Proc. of SETTA 2025, Lecture Notes in Computer Science 16458, pp.177-195, 2025
@inproceedings{meng2025efficient,title={Efficient Decomposition Identification of Deterministic Finite Automata from Examples},author={Meng, Junjie and An, Jie and Li, Yong and Turrini, Andrea and Zhan, Fanjiang Xu Naijun and Zhang, Miaomiao},booktitle={the Proc. of SETTA 2025, Lecture Notes in Computer Science 16458, pp.177-195},year={2025},}
[C21]
Runtime Enforcement of CPS against Signal Temporal Logic
Han Su, Saumya Shankar, Srinivas Pinisetty, Partha Roop, and Naijun Zhan
In the Proceedings of HSCC 2025, Article 18:1-11, 2025
One of the two Best Paper Award finalists at HSCC 2025.
@inproceedings{su2025runtime,title={Runtime Enforcement of CPS against Signal Temporal Logic},author={Su, Han and Shankar, Saumya and Pinisetty, Srinivas and Roop, Partha and Zhan, Naijun},booktitle={the Proceedings of HSCC 2025, Article 18:1-11},year={2025},}
[C22]
Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge
Yue Fang, Jie An, Zhi Jin, Xiaohong Chen, and Naijun Zhan
@inproceedings{fang2025enhancing,title={Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge},author={Fang, Yue and An, Jie and Jin, Zhi and Chen, Xiaohong and Zhan, Naijun},booktitle={the Proceedings of ACL 2025},year={2025},}
@inproceedings{xu2025calculusb,title={HpC: A Calculus for Hybrid and Mobile Systems},author={Xu, Xiong and Talpin, Jean-Pierre and Wang, Shuling and Zhan, Bohua and Liu, Xinxin and Zhan, Naijun},booktitle={OOPSLA 2025},year={2025},}
[C24]
Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System
Xiong Xu, Shuling Wang, Zekun Ji, Qiang Gao, Xiangyu Jin, Bohua Zhan, and Naijun Zhan
In the Proc. of the Festschrift of Cliff Jones’ 80th birthday, Lecture Notes in Computer Science 14781, pp.226-246, 2024
@inproceedings{xu2024case,title={Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System},author={Xu, Xiong and Wang, Shuling and Ji, Zekun and Gao, Qiang and Jin, Xiangyu and Zhan, Bohua and Zhan, Naijun},booktitle={the Proc. of the Festschrift of Cliff Jones’ 80th birthday, Lecture Notes in Computer Science 14781, pp.226-246},year={2024},}
[C25]
A Unified Framework for Quantitative Analysis of Probabilistic Programs
Shenghua Feng, Tengshun Yang, Mingshuai Chen, and Naijun Zhan
In the Proc. of Colloquium on Principles of Verification: Cycling the Probabilistic Landscape, Festschrift of Prof. Joost-Pieter Katoen’s 60th birthday, Lecture Notes in Computer Science 15260, pp.230-254, 2024
@inproceedings{feng2024unified,title={A Unified Framework for Quantitative Analysis of Probabilistic Programs},author={Feng, Shenghua and Yang, Tengshun and Chen, Mingshuai and Zhan, Naijun},booktitle={the Proc. of Colloquium on Principles of Verification: Cycling the Probabilistic Landscape, Festschrift of Prof. Joost-Pieter Katoen’s 60th birthday, Lecture Notes in Computer Science 15260, pp.230-254},year={2024},}
[C26]
Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation
Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, and Lei Ju
In the Proc. of SETTA 2024, Lecture Notes in Computer Science 15469, pp.217-235, 2024
@inproceedings{xiao2024cache,title={Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation},author={Xiao, Shangshang and Sun, Mengxia and Zhang, Wei and Zhan, Naijun and Ju, Lei},booktitle={the Proc. of SETTA 2024, Lecture Notes in Computer Science 15469, pp.217-235},year={2024},}
[C27]
The Design of Intelligent Temperature Control System of Smart House with MARS
@inproceedings{yin2024design,title={The Design of Intelligent Temperature Control System of Smart House with MARS},author={Yin, Yihao and Wu, Hao and Wang, Shuling and Xu, Xiong and Xu, Fanjiang and Zhan, Naijun},booktitle={the Proc. of SETTA 2024, Lecture Notes in Computer Science 15469, pp.217-235},year={2024},}
[C28]
Modelling and Analysis of the LatestTime Message Synchronization Policy in ROS
Chenhao Wu, Rruoxiang Li, Naijun Zhan, and Nan Guan
In Proc. of EMSOFT 2024, also appear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(11): 3576-3587, 2024
@inproceedings{wu2024modellingb,title={Modelling and Analysis of the LatestTime Message Synchronization Policy in ROS},author={Wu, Chenhao and Li, Rruoxiang and Zhan, Naijun and Guan, Nan},booktitle={Proc. of EMSOFT 2024, also appear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(11): 3576-3587},year={2024},}
[C29]
Switching Controller Synthesis for Hybrids Systems Against STL Formulas
Han Su, Shenghua Feng, Sinong Zhan, and Naijun Zhan
In Proc. of FM 2024, Lecture Notes in Computer Science 14934, pp. 229-247, 2024
@inproceedings{su2024switching,title={Switching Controller Synthesis for Hybrids Systems Against STL Formulas},author={Su, Han and Feng, Shenghua and Zhan, Sinong and Zhan, Naijun},booktitle={Proc. of FM 2024, Lecture Notes in Computer Science 14934, pp. 229-247},year={2024},}
[C30]
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, and Naijun Zhan
In Proc. of FM 2024, Lecture Notes in Computer Science 14934, pp.248-266, 2024
@inproceedings{wu2024completeness,title={On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains},author={Wu, Hao and Feng, Shenghua and Gan, Ting and Wang, Jie and Xia, Bican and Zhan, Naijun},booktitle={Proc. of FM 2024, Lecture Notes in Computer Science 14934, pp.248-266},year={2024},}
[C31]
Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, and Ting Gan
In Proc. of FM 2024, Lecture Notes in Computer Science 14933, pp.92-110, 2024
@inproceedings{wu2024nonlinear,title={Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets},author={Wu, Hao and Wang, Jie and Xia, Bican and Li, Xiakun and Zhan, Naijun and Gan, Ting},booktitle={Proc. of FM 2024, Lecture Notes in Computer Science 14933, pp.92-110},year={2024},}
[C32]
The Opacity of Timed Automata
Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, and Ichiro Hasuo
In Proc. of FM 2024, Lecture Notes in Computer Science 14933, pp.620-637, 2024
@inproceedings{an2024opacity,title={The Opacity of Timed Automata},author={An, Jie and Gao, Qiang and Wang, Lingtai and Zhan, Naijun and Hasuo, Ichiro},booktitle={Proc. of FM 2024, Lecture Notes in Computer Science 14933, pp.620-637},year={2024},}
[C33]
Improving the Reaction Latency Analysis of Message Synchronization in ROS
Chenhao Wu, Ruoxiang Li, Naijun Zhan, and Nan Guan
@inproceedings{wu2024improving,title={Improving the Reaction Latency Analysis of Message Synchronization in ROS},author={Wu, Chenhao and Li, Ruoxiang and Zhan, Naijun and Guan, Nan},booktitle={Proc. of RTCSA 2024, pp. 43-48},year={2024},}
[C34]
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, and Naijun Zhan
In (a full version). In Proc. of ICCPS 2024, pp.123-134, 2024
@inproceedings{wang2024formally,title={Formally Verified C Code Generation from Hybrid Communicating Sequential Processes},author={Wang, Shuling and Ji, Zekun and Zhan, Bohua and Xu, Xiong and Gao, Qiang and Zhan, Naijun},booktitle={(a full version). In Proc. of ICCPS 2024, pp.123-134},year={2024},}
[C35]
An Executable Semantics for Stateflow in Isabelle/HOL
Shicheng Yi, Shuling Wang, Bohua Zhan, and Naijun Zhan
In Proc. of ICFEM 2022, Lecture Notes in Computer Science 13478, pp.421-438, 2022
@inproceedings{yi2022executable,title={An Executable Semantics for Stateflow in Isabelle/HOL},author={Yi, Shicheng and Wang, Shuling and Zhan, Bohua and Zhan, Naijun},booktitle={Proc. of ICFEM 2022, Lecture Notes in Computer Science 13478, pp.421-438},year={2022},}
[C36]
Learning Deterministic One-Clock Timed Automata via Mutation Testing
Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, and Naijun Zhan
In Proc. of ATVA 2022. Lecture Notes in Computer Science 13505, pp.233-248, 2022
@inproceedings{tang2022learning,title={Learning Deterministic One-Clock Timed Automata via Mutation Testing},author={Tang, Xiaochen and Shen, Wei and Zhang, Miaomiao and An, Jie and Zhan, Bohua and Zhan, Naijun},booktitle={Proc. of ATVA 2022. Lecture Notes in Computer Science 13505, pp.233-248},year={2022},}
[C37]
Differential Games Based on Invariant Sets Generation
Bai Xue, Qiuye Wang, Naijun Zhan, Martin Frnzle, and Shenghua Feng
@inproceedings{xue2022differential,title={Differential Games Based on Invariant Sets Generation},author={Xue, Bai and Wang, Qiuye and Zhan, Naijun and Frnzle, Martin and Feng, Shenghua},booktitle={Proc. of ACC 2022, pp. 1285-1292},year={2022},}
[C38]
Formal Analysis of 5G AKMA
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, and Bifei Mao
In Proc. of SETTA 2021, Lecture Notes in Computer Science 13071, pp.102-121, 2021
@inproceedings{yang2021formal,title={Formal Analysis of 5G AKMA},author={Yang, Tengshun and Wang, Shuling and Zhan, Bohua and Zhan, Naijun and Li, Jinghui and Xiang, Shuangqing and Xiang, Zhan and Mao, Bifei},booktitle={Proc. of SETTA 2021, Lecture Notes in Computer Science 13071, pp.102-121},year={2021},}
[C39]
Reach-Avoid Analysis for Delay Differential Equations
Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu, and Li Jiao
@inproceedings{xue2021reach,title={Reach-Avoid Analysis for Delay Differential Equations},author={Xue, Bai and Bai, Yunjun and Zhan, Naijun and Liu, Wenyou and Jiao, Li},booktitle={CDC 2021, pp.1301-1307},year={2021},}
[C40]
Learning Nondeterministic Real-Time Automata
Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang
@inproceedings{an2021learningb,title={Learning Nondeterministic Real-Time Automata},author={An, Jie and Zhan, Bohua and Zhan, Naijun and Zhang, Miaomiao},booktitle={EMSOFT 2021},year={2021},}
[C41]
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, a submitted version and a full version
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen
In Proc. of CAV 2021, Lecture Notes in Computer Science 12759, pp.443-466, 2021
@inproceedings{wang2021synthesizing,title={Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, a submitted version and a full version},author={Wang, Qiuye and Chen, Mingshuai and Xue, Bai and Zhan, Naijun and Katoen, Joost-Pieter},booktitle={Proc. of CAV 2021, Lecture Notes in Computer Science 12759, pp.443-466},year={2021},}
[C42]
Modeling and Verification of Descent Guidance Control of Mars Lander
Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, and Naijun Zhan
In Proc. of RTAS 2021 (a brief industry paper), pp.457-460, 2021
@inproceedings{zhan2021modeling,title={Modeling and Verification of Descent Guidance Control of Mars Lander},author={Zhan, Bohua and Gu, Bin and Xu, Xiong and Jin, Xiangyu and Wang, Shuling and Xue, Bai and Li, Xiaofeng and Chen, Yao and Yang, Mengfei and Zhan, Naijun},booktitle={Proc. of RTAS 2021 (a brief industry paper), pp.457-460},year={2021},}
[C43]
Reach-avoid Analysis for Stochastic Discrete-time Systems
Bai Xue, Renjue Li, Naijun Zhan, and Martin Fränzle
@inproceedings{xue2021reachb,title={Reach-avoid Analysis for Stochastic Discrete-time Systems},author={Xue, Bai and Li, Renjue and Zhan, Naijun and Fränzle, Martin},booktitle={Proc. of ACC 2021, pp.4879-4885},year={2021},}
[C44]
Switching Controller Synthesis for Time-delayed Hybrid Systems under Perturbation
Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, and Naijun Zhan
@inproceedings{bai2021switchingb,title={Switching Controller Synthesis for Time-delayed Hybrid Systems under Perturbation},author={Bai, Yunjun and Gan, Ting and Jiao, Li and Xia, Bican and Xue, Bai and Zhan, Naijun},booktitle={Proc. of HSCC 2021, pp. 3:1-3:11},year={2021},}
[C45]
Probably Approximately Correct Interpolants Generation
Bai Xue and Naijun Zhan
In Proc. of SETTA 2020, Lecture Notes in Computer Science, 12153, pp. 143-159, 2020
@inproceedings{xue2020probably,title={Probably Approximately Correct Interpolants Generation},author={Xue, Bai and Zhan, Naijun},booktitle={Proc. of SETTA 2020, Lecture Notes in Computer Science, 12153, pp. 143-159},year={2020},}
[C46]
PAC learning of deterministic one-clock timed automata
Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, and Naijun Zhan
In Proc. of ICFEM 2020, Lecture Notes in Computer Science 12531, pp.129-146, 2020
@inproceedings{shen2020learning,title={PAC learning of deterministic one-clock timed automata},author={Shen, Wei and An, Jie and Zhan, Bohua and Zhang, Miaomiao and Xue, Bai and Zhan, Naijun},booktitle={Proc. of ICFEM 2020, Lecture Notes in Computer Science 12531, pp.129-146},year={2020},}
[C47]
Inner-approximating reach-avoid sets for discrete-time polynomial systems
@inproceedings{xue2020innerb,title={Inner-approximating reach-avoid sets for discrete-time polynomial systems},author={Xue, Bai and Zhan, Naijun and Fränzle, Martin},booktitle={Proc. of CDC 2020, pp. 867-873},year={2020},}
[C48]
Safety Verification for Random Ordinary Differential Equations
Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, and Bican Xia
In Proc. of EMSOFT 2020, also appear IEEE TCAD, 39(11):4090-4101, 2020
@inproceedings{xue2020safetyb,title={Safety Verification for Random Ordinary Differential Equations},author={Xue, Bai and Fränzle, Martin and Zhan, Naijun and Bogomolov, Sergiy and Xia, Bican},booktitle={Proc. of EMSOFT 2020, also appear IEEE TCAD, 39(11):4090-4101},year={2020}}
[C49]
Unbounded-time Safety Verification of Stochastic Differential Dynamics
Shenghua Feng, Mingshuai Chen, Sriram Sankaranarayanan, Bai Xue, and Naijun Zhan
In Proc. of CAV 2020, Lecture Notes in Computer Science 12224, pp.327-348, 2020
@inproceedings{feng2020unbounded,title={Unbounded-time Safety Verification of Stochastic Differential Dynamics},author={Feng, Shenghua and Chen, Mingshuai and Sankaranarayanan, Sriram and Xue, Bai and Zhan, Naijun},booktitle={Proc. of CAV 2020, Lecture Notes in Computer Science 12224, pp.327-348},year={2020},}
[C50]
Non-linear Interpolant Generation
Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, and Liyun Dai
In Proc. of CAV 2020, Lecture Notes in Computer Science 12225, pp.415-438, 2020
@inproceedings{gan2020linear,title={Non-linear Interpolant Generation},author={Gan, Ting and Xia, Bican and Xue, Bai and Zhan, Naijun and Dai, Liyun},booktitle={Proc. of CAV 2020, Lecture Notes in Computer Science 12225, pp.415-438},year={2020},}
[C51]
Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems
@inproceedings{xue2020robust,title={Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems},author={Xue, Bai and Zhan, Naijun and Li, Yangjia},booktitle={Proc. of IFAC 2020},year={2020},}
[C52]
A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations
@inproceedings{xue2020characterization,title={A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations},author={Xue, Bai and Zhan, Naijun and Li, Yangjia},booktitle={Proc. of IFAC 2020},year={2020},}
[C53]
Learning one-clock timed automata
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhan
In Proc. of TACAS 2020, Lecture Notes in Computer Science 12078, pp.444-462, 2020
@inproceedings{an2020learningb,title={Learning one-clock timed automata},author={An, Jie and Chen, Mingshuai and Zhan, Bohua and Zhan, Naijun and Zhan, Miaomiao},booktitle={Proc. of TACAS 2020, Lecture Notes in Computer Science 12078, pp.444-462},year={2020},}
[C54]
Taming delays in cyber-physical systems
Naijun Zhan
In Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852, pp. xv-xvii. (the extend abstract of an invited talk), 2019
@inproceedings{zhan2019taming,title={Taming delays in cyber-physical systems},author={Zhan, Naijun},booktitle={Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852, pp. xv-xvii. (the extend abstract of an invited talk)},year={2019},}
[C55]
Probably Approximate Safety Verification of Hybrid Dynamical Systems
Bai Xue, Martin Fraenzle, Hengjun Zhao, Naijun Zhan, and Arvind Easwaran
In Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852, pp. 236-252, 2019
@inproceedings{xue2019probably,title={Probably Approximate Safety Verification of Hybrid Dynamical Systems},author={Xue, Bai and Fraenzle, Martin and Zhao, Hengjun and Zhan, Naijun and Easwaran, Arvind},booktitle={Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852, pp. 236-252},year={2019},}
[C56]
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, and Naijun Zhan
@inproceedings{mitsch2019arch,title={ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving},author={Mitsch, Stefan and Sogokon, Andrew and Tan, Yong Kiam and Jin, Xiangyu and Zhan, Bohua and Wang, Shuling and Zhan, Naijun},booktitle={ARCH@ CPSIoTWeek 2019: 141-161},year={2019},}
[C57]
Unified Graphical Co-Modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow
@inproceedings{zhan2019unified,title={Unified Graphical Co-Modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow},author={Zhan, Haolan and Lin, Qianqian and Wang, Shuling and Talpin, Jean-Pierre and Xu, Xiong and Zhan, Naijun},booktitle={Proc. of UTP 2019, Lecture Notes in Computer Science 11885, pp. 109-129},year={2019},}
[C58]
Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue
In Proc. of CAV 2019, Lecture Notes in Computer Science 11561, pp.650-669, 2019
@inproceedings{feng2019taming,title={Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations},author={Feng, Shenghua and Chen, Mingshuai and Zhan, Naijun and Fränzle, Martin and Xue, Bai},booktitle={Proc. of CAV 2019, Lecture Notes in Computer Science 11561, pp.650-669},year={2019},}
[C59]
Formal verification of quantum algorithms using quantum Hoare logic
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan
In Proc. of CAV 2019, Lecture Notes in Computer Science 11562, pp.187-207, 2019
@inproceedings{liu2019formal,title={Formal verification of quantum algorithms using quantum Hoare logic},author={Liu, Junyi and Zhan, Bohua and Wang, Shuling and Ying, Shenggang and Liu, Tao and Li, Yangjia and Ying, Mingsheng and Zhan, Naijun},booktitle={Proc. of CAV 2019, Lecture Notes in Computer Science 11562, pp.187-207},year={2019},}
[C60]
NIL: Learning Nonlinear Interpolants
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan
In Proc. of CADE 2019, , Lecture Notes in Computer Science 11716, pp.178-196, 2019
@inproceedings{chen2019learning,title={NIL: Learning Nonlinear Interpolants},author={Chen, Mingshuai and Wang, Jian and An, Jie and Zhan, Bohua and Kapur, Deepak and Zhan, Naijun},booktitle={Proc. of CADE 2019, , Lecture Notes in Computer Science 11716, pp.178-196},year={2019},}
[C61]
Robust Invariant Sets Generation for State-Constrained Perturbed Polynomial Systems
Bai Xue, Qiuye Wang, Naijun Zhan, and Martin Fraenzle
@inproceedings{xue2019robust,title={Robust Invariant Sets Generation for State-Constrained Perturbed Polynomial Systems},author={Xue, Bai and Wang, Qiuye and Zhan, Naijun and Fraenzle, Martin},booktitle={Proc. of HSCC 2019, pp. 128-137},year={2019},}
[C62]
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, and Naijun Zhan
@inproceedings{mitsch2018arch,title={ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving},author={Mitsch, Stefan and Sogokon, Andrew and Tan, Yong Kiam and Platzer, André and Zhao, Hengjun and Jin, Xiangyu and Wang, Shuling and Zhan, Naijun},booktitle={ARCH@ADHS 2018: 110-127},year={2018},}
[C63]
The opacity of real-time automata
Lingtai Wang, Naijun Zhan, and Jie An
In Proc. of EMSOFT 2018. (Also to appear in the special issue of IEEE TCAD for EMSOFT 2018), 2018
@inproceedings{wang2018opacityb,title={The opacity of real-time automata},author={Wang, Lingtai and Zhan, Naijun and An, Jie},booktitle={Proc. of EMSOFT 2018. (Also to appear in the special issue of IEEE TCAD for EMSOFT 2018)},year={2018},}
[C64]
What’s to come is still unsure: Synthesizing synthesizers resilient to delayed reaction
Mingshuai Chen, Martin Fraenzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan
In ATVA 2018, Lecture Notes in Computer Science 11138, pp.56-74, 2018
@inproceedings{chen2018what,title={What’s to come is still unsure: Synthesizing synthesizers resilient to delayed reaction},author={Chen, Mingshuai and Fraenzle, Martin and Li, Yangjia and Mosaad, Peter N. and Zhan, Naijun},booktitle={ATVA 2018, Lecture Notes in Computer Science 11138, pp.56-74},year={2018},}
[C65]
Robust Non-termination Analysis of Numerical Software
Bai Xue, Naijun Zhan, Yangjia Li, and Qiuye Wang
In Proc. of SETTA 2018, Lecture Notes in Computer Science 10998, pp. 69-88, 2018
@inproceedings{xue2018robust,title={Robust Non-termination Analysis of Numerical Software},author={Xue, Bai and Zhan, Naijun and Li, Yangjia and Wang, Qiuye},booktitle={Proc. of SETTA 2018, Lecture Notes in Computer Science 10998, pp. 69-88},year={2018},}
[C66]
Decidability of the initial-state opacity of real-time automata
Lingtai Wang and Naijun Zhan
In Proc. of Symposium on Real-time and Hybrid Systems in Honor of Prof. Chaochen Zhou’s 80th Birthday, Lecture Notes in Computer Science 11180, pp. 40-60, 2018
@inproceedings{wang2018decidability,title={Decidability of the initial-state opacity of real-time automata},author={Wang, Lingtai and Zhan, Naijun},booktitle={Proc. of Symposium on Real-time and Hybrid Systems in Honor of Prof. Chaochen Zhou’s 80th Birthday, Lecture Notes in Computer Science 11180, pp. 40-60},year={2018},}
@inproceedings{feng2018monitoring,title={Monitoring CTMCs by multi-clock timed automata},author={Feng, Yijun and Katoen, Joost-Pieter and Li, Haokun and Xia, Bican and Zhan, Naijun},booktitle={Proc. of CAV 2018, Lecture Notes in Computer Science 10981, pp. 507-526},year={2018},}
[C68]
Model-checking continuous-time bounded extended linear duration invariants
Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, and Wang Yi
@inproceedings{an2018model,title={Model-checking continuous-time bounded extended linear duration invariants},author={An, Jie and Zhan, Naijun and Li, Xiaoshan and Zhang, Miaomiao and Yi, Wang},booktitle={Proc. of HSCC 2018, pp.81-90},year={2018},}
[C69]
Under-Approximating Reach Sets for Polynomial Continuous Systems
@inproceedings{xue2018under,title={Under-Approximating Reach Sets for Polynomial Continuous Systems},author={Xue, Bai and Fraenzle, Martin and Zhan, Naijun},booktitle={Proc. of HSCC 2018, pp.51-60},year={2018},}
[C70]
Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus
Dimitar P. Guelev, Shuling Wang, and Naijun Zhan
In Proc. of SETTA2017, Lecture Notes in Computer Science 10606, pp.110-127, 2017
@inproceedings{guelev2017compositional,title={Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus},author={Guelev, Dimitar P. and Wang, Shuling and Zhan, Naijun},booktitle={Proc. of SETTA2017, Lecture Notes in Computer Science 10606, pp.110-127},year={2017},}
[C71]
Generating SystemC code from delay HCSP
Gaogao Yan, Li Jiao, Shuling Wang, and Naijun Zhan
In Proc. of APLAS 2017, Lecture Notes in Computer Science 10695, pp.21-41, 2017
@inproceedings{yan2017generating,title={Generating SystemC code from delay HCSP},author={Yan, Gaogao and Jiao, Li and Wang, Shuling and Zhan, Naijun},booktitle={Proc. of APLAS 2017, Lecture Notes in Computer Science 10695, pp.21-41},year={2017},}
[C72]
Finding polynomial loop invariants for probabilistic programs
Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, and Bican Xia
In Proc. of ATVA 2017, Lecture Notes in Computer Science 10484, pp. 400-416, 2017
@inproceedings{feng2017finding,title={Finding polynomial loop invariants for probabilistic programs},author={Feng, Yijun and Zhang, Lijun and Jansen, David N. and Zhan, Naijun and Xia, Bican},booktitle={Proc. of ATVA 2017, Lecture Notes in Computer Science 10484, pp. 400-416},year={2017},}
[C73]
Safe over- and under-approximation of reachable sets for delay differential equations
Bai Xue, Peter Nazier Mosaad, Martin Fraenzle, Mingshuai Chen, Yangjia Li, and Naijun Zhan
In Proc. of FORMATS 2017, Lecture Notes in Computer Science 10419, pp.281-299. (It contains some mistakes, a corrected version is downloadable here), 2017
@inproceedings{xue2017safe,title={Safe over- and under-approximation of reachable sets for delay differential equations},author={Xue, Bai and Mosaad, Peter Nazier and Fraenzle, Martin and Chen, Mingshuai and Li, Yangjia and Zhan, Naijun},booktitle={Proc. of FORMATS 2017, Lecture Notes in Computer Science 10419, pp.281-299. (It contains some mistakes, a corrected version is downloadable here)},year={2017},}
[C74]
Approximate bisimulation and discretization of Hybrid CSP
Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, and Naijun Zhan
In Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp.702-720, 2016
@inproceedings{yan2016approximate,title={Approximate bisimulation and discretization of Hybrid CSP},author={Yan, Gaogao and Jiao, Li and Li, Yangjia and Wang, Shuling and Zhan, Naijun},booktitle={Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp.702-720},year={2016},}
[C75]
Validated simulation-based verification of delayed differential dynamics
Mingshuai Chen, Martin Fraenzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan
In Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp.137-154, 2016
@inproceedings{chen2016validated,title={Validated simulation-based verification of delayed differential dynamics},author={Chen, Mingshuai and Fraenzle, Martin and Li, Yangjia and Mosaad, Peter N. and Zhan, Naijun},booktitle={Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp.137-154},year={2016},}
[C76]
A two-way path between formal and informal design of embedded systems
Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, and Naijun Zhan
In Proc. of UTP 2016, Lecture Notes in Computer Science 10134, pp.65-92, 2016
@inproceedings{chen2016path,title={A two-way path between formal and informal design of embedded systems},author={Chen, Mingshuai and Ravn, Anders P. and Wang, Shuling and Yang, Mengfei and Zhan, Naijun},booktitle={Proc. of UTP 2016, Lecture Notes in Computer Science 10134, pp.65-92},year={2016},}
[C77]
Computing reachable sets of linear vector fields revisited
@inproceedings{gan2016computing,title={Computing reachable sets of linear vector fields revisited},author={Gan, Ting and Chen, Mingshuai and Li, Yangjia and Xia, Bican and Zhan, Naijun},booktitle={Proc. of ECC 2016, pp.419-426},year={2016},}
[C78]
Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
@inproceedings{gan2016interpolant,title={Interpolant synthesis for quadratic polynomial inequalities and combination with EUF},author={Gan, Ting and Dai, Liyun and Xia, Bican and Zhan, Naijun and Kapur, Deepak and Chen, Mingshuai},booktitle={Proc. of IJCAR 2016, Lecture Notes in Computer Science 9706, pp.195-212},year={2016},}
[C79]
Extending Hybrid CSP with Probability and Stochasticity
Yu Peng, Shuling Wang, Naijun Zhan, and Lijun Zhang
In Proc. SETTA 2015, Lecture Notes in Computer Science 9409, pp.87-102, 2015
@inproceedings{peng2015extending,title={Extending Hybrid CSP with Probability and Stochasticity},author={Peng, Yu and Wang, Shuling and Zhan, Naijun and Zhang, Lijun},booktitle={Proc. SETTA 2015, Lecture Notes in Computer Science 9409, pp.87-102},year={2015},}
[C80]
An improved HHL prover: An interactive theorem prover for hybrid systems
S. Wang, N. Zhan, and L. Zou
In Proc. of ICFEM 2015, Lecture Notes in Computer Science 9407, pp.282-399, 2015
@inproceedings{wang2015improved,title={An improved HHL prover: An interactive theorem prover for hybrid systems},author={Wang, S. and Zhan, N. and Zou, L.},booktitle={Proc. of ICFEM 2015, Lecture Notes in Computer Science 9407, pp.282-399},year={2015},}
[C81]
Decidability of the reachability for a family of linear vector fields
@inproceedings{gan2015decidability,title={Decidability of the reachability for a family of linear vector fields},author={Gan, Ting and Chen, Mingshuai and Dai, Liyun and Xia, Bican and Zhan, Naijun},booktitle={Proc. of ATVA 2015, Lecture Notes in Computer Science 9364, pp.482-499},year={2015},}
[C82]
Formal verification of Simulink/Stateflow diagrams
Liang Zou, Naijun Zhan, Shuling Wang, and Martin Fraenzle
In Proc. of ATVA 2015, Lecture Notes in Computer Science 9364, pp.482-499, 2015
@inproceedings{zou2015formal,title={Formal verification of Simulink/Stateflow diagrams},author={Zou, Liang and Zhan, Naijun and Wang, Shuling and Fraenzle, Martin},booktitle={Proc. of ATVA 2015, Lecture Notes in Computer Science 9364, pp.482-499},year={2015},}
[C83]
Automatic stability and safety verification for delay differential equations
Liang Zou, Martin Fraenzle, Naijun Zhan, and Peter Nazier Mosaad
In Proc. of CAV 2015, Lecture Notes in Computer Science 9364, pp.338-355, 2015
@inproceedings{zou2015automatic,title={Automatic stability and safety verification for delay differential equations},author={Zou, Liang and Fraenzle, Martin and Zhan, Naijun and Mosaad, Peter Nazier},booktitle={Proc. of CAV 2015, Lecture Notes in Computer Science 9364, pp.338-355},year={2015},}
[C84]
Abstraction of elementary hybrid systems by variable transformation
Jiang Liu, Naijun Zhan, Hengjun Zhao, and Liang Zou
In Proc. of FM 2015, Lecture Notes in Computer Science 9109, pp.360-377, 2015
@inproceedings{liu2015abstraction,title={Abstraction of elementary hybrid systems by variable transformation},author={Liu, Jiang and Zhan, Naijun and Zhao, Hengjun and Zou, Liang},booktitle={Proc. of FM 2015, Lecture Notes in Computer Science 9109, pp.360-377},year={2015},}
[C85]
Formal verification of Simulink/Stateflow diagrams
@inproceedings{zhan2014formal,title={Formal verification of Simulink/Stateflow diagrams},author={Zhan, Naijun and Zou, Liang},booktitle={Proc. of ESWEEK 2014 (abstract only)},year={2014}}
[C86]
An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling
Ehsan Ahmad, Brian Larson, Stephen Barrett, Naijun Zhan, and Yunwei Dong
@inproceedings{ahmad2014aadl,title={An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling},author={Ahmad, Ehsan and Larson, Brian and Barrett, Stephen and Zhan, Naijun and Dong, Yunwei},booktitle={Proc. of HILT 2014, pp.29-38},year={2014},}
[C87]
Adding Formal Meanings to AADL Models with Hybrid Annex
Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan, and Liang Zou
In Proc. of FACS 2014, Lecture Notes in Computer Science 8997, pp.228-247, 2014
@inproceedings{ahmad2014adding,title={Adding Formal Meanings to AADL Models with Hybrid Annex},author={Ahmad, Ehsan and Dong, Yunwei and Wang, Shuling and Zhan, Naijun and Zou, Liang},booktitle={Proc. of FACS 2014, Lecture Notes in Computer Science 8997, pp.228-247},year={2014},}
[C88]
Formal verification of a descent guidance control program of a lunar lander
Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, and Yao Chen
In Proc. of FM 2014, Lecture Notes in Computer Science 8442, pp.733-748, 2014
@inproceedings{zhao2014formal,title={Formal verification of a descent guidance control program of a lunar lander},author={Zhao, Hengjun and Yang, Mengfei and Zhan, Naijun and Gu, Bin and Zou, Liang and Chen, Yao},booktitle={Proc. of FM 2014, Lecture Notes in Computer Science 8442, pp.733-748},year={2014},}
[C89]
Towards a failure model of software components
Ruzhen Dong and Naijun Zhan
In Proc. of FACS 2013, Lecture Notes in Computer Science 8348, pp.119-136, 2013
@inproceedings{dong2013towards,title={Towards a failure model of software components},author={Dong, Ruzhen and Zhan, Naijun},booktitle={Proc. of FACS 2013, Lecture Notes in Computer Science 8348, pp.119-136},year={2013},}
[C90]
Super-dense computation in verification of HCSP processes
Dimitar P. Guelev, Shuling Wang, Naijun Zhan, and Chaochen Zhou
In Proc. of FACS 2013, Lecture Notes in Computer Science 8348, pp.13-22, 2013
@inproceedings{guelev2013super,title={Super-dense computation in verification of HCSP processes},author={Guelev, Dimitar P. and Wang, Shuling and Zhan, Naijun and Zhou, Chaochen},booktitle={Proc. of FACS 2013, Lecture Notes in Computer Science 8348, pp.13-22},year={2013},}
[C91]
Verifying Simulink diagrams via a Hybrid Hoare Logic prover
Liang Zou, Naijun Zhan, Shuling Wang, Martin Fraenzle, and Shengchao Qin
@inproceedings{zou2013verifying,title={Verifying Simulink diagrams via a Hybrid Hoare Logic prover},author={Zou, Liang and Zhan, Naijun and Wang, Shuling and Fraenzle, Martin and Qin, Shengchao},booktitle={Proc. of EMSOFT 2013, pp.1-10},year={2013},}
[C92]
Verifying Chinese train control system under a combined scenario by theorem proving
Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, and Yu Lei
In Proc. of VSTTE 2013, Lecture Notes in Computer Science 8164, pp.262-280, 2013
@inproceedings{zou2013verifyingb,title={Verifying Chinese train control system under a combined scenario by theorem proving},author={Zou, Liang and Lv, Jidong and Wang, Shuling and Zhan, Naijun and Tang, Tao and Yuan, Lei and Lei, Yu},booktitle={Proc. of VSTTE 2013, Lecture Notes in Computer Science 8164, pp.262-280},year={2013},}
[C93]
A CSL model checker for continuous-time markov chains
Yang Gao, Ernst Moritz Hahn, Naijun Zhan, and Lijun Zhang
In Proc. of ATVA 2013, Lecture Notes in Computer Science 8172, pp.464-468, 2013
@inproceedings{gao2013modelb,title={A CSL model checker for continuous-time markov chains},author={Gao, Yang and Hahn, Ernst Moritz and Zhan, Naijun and Zhang, Lijun},booktitle={Proc. of ATVA 2013, Lecture Notes in Computer Science 8172, pp.464-468},year={2013},}
[C94]
An interface model of software components
Ruzhen Dong, Naijun Zhan, and Liang Zhao
In Proc. of ICTAC 2013, Lecture Notes in Computer Science 8049, pp.159-176, 2013
@inproceedings{dong2013interface,title={An interface model of software components},author={Dong, Ruzhen and Zhan, Naijun and Zhao, Liang},booktitle={Proc. of ICTAC 2013, Lecture Notes in Computer Science 8049, pp.159-176},year={2013},}
[C95]
Synthesizing switching controllers for hybrid systems by generating invariants
Hengjun Zhao, Naijun Zhan, and Deepak Kapur
In Proc. of the Jifeng Festschrift, Lecture Notes in Computer Science 8051, pp.354-373, 2013
@inproceedings{zhao2013synthesizing,title={Synthesizing switching controllers for hybrid systems by generating invariants},author={Zhao, Hengjun and Zhan, Naijun and Kapur, Deepak},booktitle={Proc. of the Jifeng Festschrift, Lecture Notes in Computer Science 8051, pp.354-373},year={2013},}
[C96]
Generating non-linear interpolants by semi-definite programming
Liyun Dai, Bican Xia, and Naijun Zhan
In Proc. of CAV 2013, Lecture Notes in Computer Science 8044, pp.364-380, 2013
@inproceedings{dai2013generating,title={Generating non-linear interpolants by semi-definite programming},author={Dai, Liyun and Xia, Bican and Zhan, Naijun},booktitle={Proc. of CAV 2013, Lecture Notes in Computer Science 8044, pp.364-380},year={2013},}
[C97]
Bounded model-checking of discrete Duration Calculus
Quan Zu, Miaomiao Zhang, Jiaqi Zhu, and Naijun Zhan
@inproceedings{zu2013bounded,title={Bounded model-checking of discrete Duration Calculus},author={Zu, Quan and Zhang, Miaomiao and Zhu, Jiaqi and Zhan, Naijun},booktitle={Proc. of HSCC 2013, pp.213-222},year={2013},}
[C98]
A “hybrid” approach for synthesizing optimal controllers of hybrid systems: A Case study of the oil pump industrial example
Hengjun Zhao, Naijun Zhan, Deepak Kapur, and Kim G. Larsen
In Proc. of FM 2012, Lecture Notes in Computer Science 7436, pp.471-485, 2012, 2012
@inproceedings{zhao2012hybrid,title={A “hybrid” approach for synthesizing optimal controllers of hybrid systems: A Case study of the oil pump industrial example},author={Zhao, Hengjun and Zhan, Naijun and Kapur, Deepak and Larsen, Kim G.},booktitle={Proc. of FM 2012, Lecture Notes in Computer Science 7436, pp.471-485, 2012},year={2012},}
[C99]
An assume/guarantee based compositional calculus for Hybrid CSP
Shuling Wang, Naijun Zhan, and Dimitar Guelev
In A keynotes of TAMC 2012, Lecture Notes in Computer Science 7287, pp.72-83, 2012
@inproceedings{wang2012assume,title={An assume/guarantee based compositional calculus for Hybrid CSP},author={Wang, Shuling and Zhan, Naijun and Guelev, Dimitar},booktitle={A keynotes of TAMC 2012, Lecture Notes in Computer Science 7287, pp.72-83},year={2012},}
[C100]
Unblockable compositions of software components
Ruzhen Dong, Johannes Farber, Zhiming Liu, Jiri Srba, Naijun Zhan, and Jiaqi Zhu
@inproceedings{dong2012unblockable,title={Unblockable compositions of software components},author={Dong, Ruzhen and Farber, Johannes and Liu, Zhiming and Srba, Jiri and Zhan, Naijun and Zhu, Jiaqi},booktitle={Proc. of CBSE 2012, ACM SIGSOFT},year={2012},}
[C101]
Computing semi-algebraic invariants for polynomial dynamical systems
Jiang Liu, Naijun Zhan, and Hengjun Zhao
In Proc. of EMSOFT 2011, pp.97-106, ACM Press, 2011
@inproceedings{liu2011computing,title={Computing semi-algebraic invariants for polynomial dynamical systems},author={Liu, Jiang and Zhan, Naijun and Zhao, Hengjun},booktitle={Proc. of EMSOFT 2011, pp.97-106, ACM Press},year={2011},}
[C102]
Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
@inproceedings{liu2011automatically,title={Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems},author={Liu, Jiang and Zhan, Naijun and Zhao, Hengjun},booktitle={Proc. of MACIS 2011, pp.162-177},year={2011}}
@inproceedings{liu2010calculus,title={A calculus for HCSP},author={Liu, Jiang and Lv, Jidong and Quan, Zhao and Zhan, Naijun and Zhao, Hengjun and Zhou, Chaochen and Zou, Liang},booktitle={A keynotes of APLAS 2010, Lecture Notes in Computer Science 6461, pp. 1-15},year={2010},}
[C105]
Model checking linear duration invariants of networks of automata
Miaomiao Zhang, Zhiming Liu, and Naijun Zhan
In Proc. FSEN 2009, Lecture Notes in Computer Science 5961 pp.244-259, 2009
@inproceedings{zhang2009model,title={Model checking linear duration invariants of networks of automata},author={Zhang, Miaomiao and Liu, Zhiming and Zhan, Naijun},booktitle={Proc. FSEN 2009, Lecture Notes in Computer Science 5961 pp.244-259},year={2009},}
[C106]
Refinement and composition of components in rCOS
Naijun Zhan, Eoun-Yound Kang, and Zhiming Liu
In Proc. of UTP 2008, Lecture Notes in Computer Science 5713, pp.238-257, 2008
@inproceedings{zhan2008refinement,title={Refinement and composition of components in rCOS},author={Zhan, Naijun and Kang, Eoun-Yound and Liu, Zhiming},booktitle={Proc. of UTP 2008, Lecture Notes in Computer Science 5713, pp.238-257},year={2008},}
[C107]
Program verification by reduction to semi-algebraic systems solving
Bican Xia, Lu Yang, and Naijun Zhan
In Proc. of ISoLA 2008, CCIS 17, Springer-Verlag, pp277-291, 2008
@inproceedings{xia2008program,title={Program verification by reduction to semi-algebraic systems solving},author={Xia, Bican and Yang, Lu and Zhan, Naijun},booktitle={Proc. of ISoLA 2008, CCIS 17, Springer-Verlag, pp277-291},year={2008},}
[C108]
Modelling with Relational Calculus of Object and Component Systems - rCOS
Zhenbang Chen, Abdel Hakim Hannousse, Dang Van Hung, Istvan Knoll, Xiaoshan Li, Zhiming Liu, Yang Liu, Qu Nan, Joseph C. Okika, Anders P. Ravn, Volker Stolz, Lu Yang, and Naijun Zhan
In Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145, 2007
@inproceedings{chen2007modelling,title={Modelling with Relational Calculus of Object and Component Systems - rCOS},author={Chen, Zhenbang and Hannousse, Abdel Hakim and Hung, Dang Van and Knoll, Istvan and Li, Xiaoshan and Liu, Zhiming and Liu, Yang and Nan, Qu and Okika, Joseph C. and Ravn, Anders P. and Stolz, Volker and Yang, Lu and Zhan, Naijun},booktitle={Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145},year={2007},}
[C109]
A model of compoent-based programming
Xin Chen, Jifeng He, Zhiming Liu, and Naijun Zhan
In Proc. Of FSEN 2007, Lecture Notes in Computer Science 4774, 2007
@inproceedings{chen2007model,title={A model of compoent-based programming},author={Chen, Xin and He, Jifeng and Liu, Zhiming and Zhan, Naijun},booktitle={Proc. Of FSEN 2007, Lecture Notes in Computer Science 4774},year={2007},}
[C110]
Reducing polynomial invariant generation to semi-algebraic systems solving
Yinghua Chen, Bican Xia, Lu Yang, and Naijun Zhan
In Proc. of Festschrift Symposium in honour of Dines Bjorner and Zhou Chaochen, Lecture Notes in Computer Science 4700, 2007
@inproceedings{chen2007reducing,title={Reducing polynomial invariant generation to semi-algebraic systems solving},author={Chen, Yinghua and Xia, Bican and Yang, Lu and Zhan, Naijun},booktitle={Proc. of Festschrift Symposium in honour of Dines Bjorner and Zhou Chaochen, Lecture Notes in Computer Science 4700},year={2007},}
[C111]
Discovering non-linear ranking functions by solving semi-algebraic systems
Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, and Chaochen Zhou
In Proc. of ICTAC 2007, Lecture Notes in Computer Science 4711, 2007
@inproceedings{chen2007discovering,title={Discovering non-linear ranking functions by solving semi-algebraic systems},author={Chen, Yinghua and Xia, Bican and Yang, Lu and Zhan, Naijun and Zhou, Chaochen},booktitle={Proc. of ICTAC 2007, Lecture Notes in Computer Science 4711},year={2007},}
[C112]
Connecting algebraical and logical descriptions of concurrent systems
Naijun Zhan
In the Proc. of ISoLA 2006, IEEE Computer Society Press, 2006
@inproceedings{zhan2006connecting,title={Connecting algebraical and logical descriptions of concurrent systems},author={Zhan, Naijun},booktitle={the Proc. of ISoLA 2006, IEEE Computer Society Press},year={2006},}
[C113]
Towards a theory of component-based real-time systems
Naijun Zhan, Dang Van Hung, Zhiming Liu, and Xiaoshan Li
In the proc. AWCVS 2006, preliminary proceedings as number 348 in UNU-IIST Reports, P.O.Box 3058, Macau, 2006
@inproceedings{zhan2006towards,title={Towards a theory of component-based real-time systems},author={Zhan, Naijun and Hung, Dang Van and Liu, Zhiming and Li, Xiaoshan},booktitle={the proc. AWCVS 2006, preliminary proceedings as number 348 in UNU-IIST Reports, P.O.Box 3058, Macau},year={2006}}
[C114]
Compositionality of fixpoint logic with chop
Naijun Zhan and Jinzhao Wu
In the Proc. of ICTAC 2005, Lecture Notes in Computer Science 3722, pp.136-150, 2005
@inproceedings{zhan2005compositionality,title={Compositionality of fixpoint logic with chop},author={Zhan, Naijun and Wu, Jinzhao},booktitle={the Proc. of ICTAC 2005, Lecture Notes in Computer Science 3722, pp.136-150},year={2005},}
[C115]
Deriving nondeterminism from conjunction and disjunction
Naijun Zhan and Mila Majster-Cederbaum
In the proc. of 25th IFIPWG 6.1 International Conference on Formal Techniques on Networked and Distributed Systems (FORTE 2005), Lecture Notes in Computer Science 3731, pp. 351-365, 2005
@inproceedings{zhan2005deriving,title={Deriving nondeterminism from conjunction and disjunction},author={Zhan, Naijun and Majster-Cederbaum, Mila},booktitle={the proc. of 25th IFIPWG 6.1 International Conference on Formal Techniques on Networked and Distributed Systems (FORTE 2005), Lecture Notes in Computer Science 3731, pp. 351-365},year={2005},}
[C116]
Program verification by using DISCOVERER
Lu Yang, Naijun Zhan, Bican Xia, and Chaochen Zhou
In the Proc. of VSTTE 2005, Lecture Notes in Computer Science 4171, pp.528-538, 2005
@inproceedings{yang2005program,title={Program verification by using DISCOVERER},author={Yang, Lu and Zhan, Naijun and Xia, Bican and Zhou, Chaochen},booktitle={the Proc. of VSTTE 2005, Lecture Notes in Computer Science 4171, pp.528-538},year={2005},}
[C117]
Refinement of actions for real-time concurrent systems with causal ambiguity
Mila Majster-Cederbaum, Jinzhao Wu, Houguang Yue, and Naijun Zhan
In the Proc. of ICFEM 2004, Lecture Notes in Computer Science 3308, pp. 449-463, 2004
@inproceedings{majstercederbaum2004refinement,title={Refinement of actions for real-time concurrent systems with causal ambiguity},author={Majster-Cederbaum, Mila and Wu, Jinzhao and Yue, Houguang and Zhan, Naijun},booktitle={the Proc. of ICFEM 2004, Lecture Notes in Computer Science 3308, pp. 449-463},year={2004},}
[C118]
Combining hierarchical specification with hierarchical implementation
Naijun Zhan
In the Proc. of ASIAN 2003, Lecture Notes in Computer Science 2896, pp. 110-124, 2003
@inproceedings{zhan2003combining,title={Combining hierarchical specification with hierarchical implementation},author={Zhan, Naijun},booktitle={the Proc. of ASIAN 2003, Lecture Notes in Computer Science 2896, pp. 110-124},year={2003},}
[C119]
Action refinement from a logical point of view
M. Majster-Cederbaum, Naijun Zhan, and Harald Fecher
In the Proc. of VMCAI 2003, Lecture Notes in Computer Science 2575, pp.253-267, 2003
@inproceedings{majstercederbaum2003action,title={Action refinement from a logical point of view},author={Majster-Cederbaum, M. and Zhan, Naijun and Fecher, Harald},booktitle={the Proc. of VMCAI 2003, Lecture Notes in Computer Science 2575, pp.253-267},year={2003},}
[C120]
Automatic synthesis of the DC specifications of Lip synchronization protocol
Huandong Ma, Liang Li, Jianzhong Wang, and Naijun Zhan
In the proc. of APSEC 2001, IEEE Computer Society Press, 2001
@inproceedings{ma2001automatic,title={Automatic synthesis of the DC specifications of Lip synchronization protocol},author={Ma, Huandong and Li, Liang and Wang, Jianzhong and Zhan, Naijun},booktitle={the proc. of APSEC 2001, IEEE Computer Society Press},year={2001}}
[C121]
Completeness of higher-order duration calculus
Naijun Zhan
In the proc. of CSL 2000, Lecture Notes in Computer Science 1863, 2000
@inproceedings{zhan2000completeness,title={Completeness of higher-order duration calculus},author={Zhan, Naijun},booktitle={the proc. of CSL 2000, Lecture Notes in Computer Science 1863},year={2000},}
[C122]
Another formal proof for deadline driven scheduler
Naijun Zhan
In the Proc. of RTCSA’00, IEEE Computer Society Press, 2000
@inproceedings{zhan2000another,title={Another formal proof for deadline driven scheduler},author={Zhan, Naijun},booktitle={the Proc. of RTCSA'00, IEEE Computer Society Press},year={2000}}
[C123]
A higher-order duration calculus
Chaochen Zhou, Dimitar P. Guelev, and Naijun Zhan
In the Proc. of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, 13-15 September, 1999, 1999
@inproceedings{zhou1999higher,title={A higher-order duration calculus},author={Zhou, Chaochen and Guelev, Dimitar P. and Zhan, Naijun},booktitle={the Proc. of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, 13-15 September, 1999},year={1999}}
[C124]
A formal proof of the rate monotonic scheduler
Shuzhen Dong, Qiwen Xu, and Naijun Zhan
In the Proc. of RTCSA 1999. IEEE Computer Society Press, 1999
@inproceedings{dong1999formal,title={A formal proof of the rate monotonic scheduler},author={Dong, Shuzhen and Xu, Qiwen and Zhan, Naijun},booktitle={the Proc. of RTCSA 1999. IEEE Computer Society Press},year={1999}}