Naijun Zhan - RankMe

218 papers A* 2A 4B 19C 18Misc 11Journal 109Unranked 50

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Exact Moment Estimation of Stochastic Differential Dynamics. CoRR Shenghua Feng, Jie An, Naijun Zhan, Fanjiang Xu
2026	C	`ed.`	Formal Methods and Software Engineering - 26th International Conference on Formal Engineering Methods, ICFEM 2025, Hangzhou, China, November 10-13, 2025, Proceedings ICFEM Étienne André, Jingyi Wang, Naijun Zhan
2026	J	`jnl`	Formal design of safety-critical systems with MARS. J. Syst. Archit. Yihao Yin, Hao Wu, Wan Liu, Shuling Wang, Xiong Xu, Wang Lin, Fanjiang Xu, Naijun Zhan
2026	J	`jnl`	Formal semantics for hierarchical Simulink diagrams in Isabelle/HOL. J. Syst. Archit. Yuzhen Qi, Shuling Wang, Xing Li, Bohua Zhan, Naijun Zhan
2026	J	`jnl`	Modeling and Verification of Hybrid Systems by Extending AADL. ACM Trans. Softw. Eng. Methodol. Xiong Xu, Ehsan Ahmad, Shuling Wang, Xiangyu Jin, Bohua Zhan, Naijun Zhan
2026	J	`jnl`	Piecewise Analysis of Probabilistic Programs via 𝑘-Induction. Proc. ACM Program. Lang. Tengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan, Jingyu Ke, Shiyang Wu
2026	—	`conf`	Quantifier Elimination Meets Treewidth. TACAS (1) Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan
2026	J	`jnl`	Quantifier Elimination Meets Treewidth. CoRR Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan
2026	A*	`conf`	RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation. AAAI Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan
2025	J	`jnl`	Active learning of deterministic timed automata via timed classification tree. Sci. China Inf. Sci. Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang, Jie An, Naijun Zhan
2025	J	`jnl`	Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries. CoRR Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, Bin Gu
2025	J	`jnl`	Derivative-Agnostic Inference of Nonlinear Hybrid Systems. CoRR Hengzhi Yu, Bohan Ma, Mingshuai Chen, Jie An, Bin Gu, Naijun Zhan, Jianwei Yin
2025	J	`jnl`	Efficient Decomposition Identification of Deterministic Finite Automata from Examples. CoRR Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang
2025	—	`conf`	Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. ACL (Findings) Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan
2025	J	`jnl`	Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. CoRR Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan
2025	C	`conf`	Formal Design of Safety-critical Embedded Systems. MEMOCODE Naijun Zhan
2025	J	`jnl`	HpC: A Calculus for Hybrid and Mobile Systems - Full Version. CoRR Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, Naijun Zhan
2025	J	`jnl`	HpC: A Calculus for Hybrid and Mobile Systems. Proc. ACM Program. Lang. Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, Naijun Zhan
2025	—	`conf`	Learning Subject to Constraints via Abstract Gradient Descent. NeuS Shiwen Yu, Wanwei Liu, Zengyu Liu, Liqian Chen, Ting Wang, Naijun Zhan, Ji Wang
2025	J	`jnl`	NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool. CoRR Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao
2025	A	`conf`	On Synthesis of Timed Regular Expressions. RTSS Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang
2025	J	`jnl`	On Synthesis of Timed Regular Expressions. CoRR Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang
2025	J	`jnl`	RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation. CoRR Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan
2025	—	`conf`	Runtime Enforcement of CPS against Signal Temporal Logic. HSCC Han Su, Saumya Shankar, Srinivas Pinisetty, Partha S. Roop, Naijun Zhan
2025	J	`jnl`	Runtime Enforcement of CPS against Signal Temporal Logic. CoRR Han Su, Saumya Shankar, Srinivas Pinisetty, Partha S. Roop, Naijun Zhan
2025	J	`jnl`	Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. ACM Trans. Program. Lang. Syst. Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhi-Hong Yang
2025	J	`jnl`	WCET Estimation for CNN Inference on FPGA SoC With Multi-DPU Engines. IEEE Trans. Parallel Distributed Syst. Wei Zhang, Yunlong Yu, Xiao Jiang, Nan Guan, Naijun Zhan, Lei Ju
2024	—	`conf`	A Unified Framework for Quantitative Analysis of Probabilistic Programs. Principles of Verification (1) Shenghua Feng, Tengshun Yang, Mingshuai Chen, Naijun Zhan
2024	J	`jnl`	A decision procedure for string constraints with string/integer conversion and flat regular constraints. Acta Informatica Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, Naijun Zhan
2024	Misc	`conf`	Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation. SETTA Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju
2024	—	`ch.`	Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System. The Practice of Formal Methods (II) Xiong Xu, Shuling Wang, Zekun Ji, Qiang Gao, Xiangyu Jin, Bohua Zhan, Naijun Zhan
2024	—	`conf`	Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. ICCPS Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao, Naijun Zhan
2024	J	`jnl`	Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. CoRR Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan
2024	J	`jnl`	HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. CoRR Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
2024	B	`conf`	Improving the Reaction Latency Analysis of Message Synchronization in ROS. RTCSA Chenhao Wu, Ruoxiang Li, Naijun Zhan, Nan Guan
2024	J	`jnl`	Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. CoRR Bohua Zhan, Xiong Xu, Qiang Gao, Zekun Ji, Xiangyu Jin, Shuling Wang, Naijun Zhan
2024	J	`jnl`	Modeling and Analysis of the LatestTime Message Synchronization Policy in ROS. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Chenhao Wu, Ruoxiang Li, Naijun Zhan, Nan Guan
2024	—	`conf`	Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. FM (1) Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan
2024	J	`jnl`	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets. CoRR Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan
2024	—	`conf`	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. FM (2) Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan
2024	J	`jnl`	Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. CoRR Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, Shiyang Wu
2024	J	`jnl`	Preface to the Special Issue on Formal Methods and Applications. Int. J. Softw. Informatics Qinxiang Cao, Fu Song, Naijun Zhan
2024	J	`jnl`	Reach-Avoid Analysis for Polynomial Stochastic Differential Equations. IEEE Trans. Autom. Control. Bai Xue, Naijun Zhan, Martin Fränzle
2024	J	`jnl`	Reach-Avoid Verification Based on Convex Optimization. IEEE Trans. Autom. Control. Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu
2024	J	`jnl`	Reset controller synthesis: a correct-by-construction way to the design of CPS. Res. Dir. Cyber Phys. Syst. Naijun Zhan, Han Su, Mengfei Yang, Bin Gu
2024	—	`conf`	Switching Controller Synthesis for Hybrid Systems Against STL Formulas. FM (2) Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan
2024	J	`jnl`	Switching Controller Synthesis for Hybrid Systems Against STL Formulas. CoRR Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan
2024	Misc	`conf`	The Design of Intelligent Temperature Control System of Smart House with MARS. SETTA Yihao Yin, Hao Wu, Shuling Wang, Xiong Xu, Fanjiang Xu, Naijun Zhan
2024	—	`conf`	The Opacity of Timed Automata. FM (1) Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo
2023	J	`jnl`	A Generalized Hybrid Hoare Logic. CoRR Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin
2023	J	`jnl`	A denotational semantics of Simulink with higher-order UTP. J. Log. Algebraic Methods Program. Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan
2023	J	`jnl`	Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. CoRR Jiang Liu, Han Su, Yunjun Bai, Bin Gu, Bai Xue, Mengfei Yang, Naijun Zhan
2023	J	`jnl`	Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. CoRR Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan
2023	J	`jnl`	Introduction to the Special Section on FM 2021. Formal Aspects Comput. Marieke Huisman, Corina S. Pasareanu, Naijun Zhan
2023	J	`jnl`	Lower Bounds for Possibly Divergent Probabilistic Programs. CoRR Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
2023	J	`jnl`	Lower Bounds for Possibly Divergent Probabilistic Programs. Proc. ACM Program. Lang. Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
2023	J	`jnl`	Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. CoRR Han Su, Jiyu Zhu, Shenghua Feng, Yunjun Bai, Bin Gu, Jiang Liu, Mengfei Yang, Naijun Zhan
2023	J	`jnl`	Safety guarantee for time-delay systems with disturbances. Sci. China Inf. Sci. Wenyou Liu, Yunjun Bai, Li Jiao, Naijun Zhan
2023	J	`jnl`	Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. ACM Trans. Softw. Eng. Methodol. Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan
2023	J	`jnl`	Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. CoRR Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhi-Hong Yang
2022	J	`jnl`	Defensive Design of Saturating Counters Based on Differential Privacy. CoRR Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan
2022	C	`conf`	Differential Games Based on Invariant Sets Generation. ACC Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng
2022	J	`jnl`	Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. Inf. Comput. Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
2022	J	`jnl`	Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming. CoRR Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
2022	J	`jnl`	Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). J. Syst. Archit. Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
2022	B	`conf`	Learning Deterministic One-Clock Timed Automata via Mutation Testing. ATVA Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan
2022	C	`conf`	Machine-Checked Executable Semantics of Stateflow. ICFEM Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
2022	J	`jnl`	Machine-checked executable semantics of Stateflow. CoRR Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
2022	J	`jnl`	Preface for the formal methods in system design special issue on 'Formal Methods 2021'. Formal Methods Syst. Des. Marieke Huisman, Corina S. Pasareanu, Naijun Zhan
2022	J	`jnl`	Reach-Avoid Analysis for Stochastic Differential Equations. CoRR Bai Xue, Naijun Zhan, Martin Fränzle
2022	J	`jnl`	Reach-avoid Verification Based on Convex Optimization. CoRR Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu
2022	J	`jnl`	Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. IEEE Trans. Autom. Control. Bai Xue, Naijun Zhan
2022	J	`jnl`	Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theor. Comput. Sci. Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan
2021	—	`conf`	ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
2021	A	`conf`	Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. RTAS Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan
2021	Misc	`conf`	Formal Analysis of 5G AKMA. SETTA Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
2021	B	`ed.`	Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings FM Marieke Huisman, Corina S. Pasareanu, Naijun Zhan
2021	J	`jnl`	Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control. Acta Informatica Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
2021	J	`jnl`	Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
2021	J	`jnl`	Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
2021	J	`jnl`	Learning real-time automata. Sci. China Inf. Sci. Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
2021	J	`jnl`	Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. IEEE Trans. Autom. Control. Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan
2021	—	`conf`	Reach-Avoid Analysis for Delay Differential Equations. CDC Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu, Li Jiao
2021	C	`conf`	Reach-avoid Analysis for Stochastic Discrete-time Systems. ACC Bai Xue, Renjue Li, Naijun Zhan, Martin Fränzle
2021	J	`jnl`	Special issue on design of embedded software and systems (SI: ICESS19). J. Syst. Archit. Arvind Easwaran, Qi Zhu, Naijun Zhan
2021	J	`jnl`	Switching Controller Synthesis for Delay Hybrid Systems under Perturbations. CoRR Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan
2021	—	`conf`	Switching controller synthesis for delay hybrid systems under perturbations. HSCC Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan
2021	—	`conf`	Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CAV (1) Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
2021	J	`jnl`	Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CoRR Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
2021	J	`jnl`	Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. SIAM J. Control. Optim. Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She
2020	—	`conf`	ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. ARCH Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
2020	J	`jnl`	Automatically Generating SystemC Code from HCSP Formal Models. ACM Trans. Softw. Eng. Methodol. Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, Naijun Zhan
2020	J	`jnl`	From model to implementation: a network algorithm programming language. Sci. China Inf. Sci. Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, Ting Gan
2020	J	`jnl`	Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. IEEE Trans. Autom. Control. Bai Xue, Martin Fränzle, Naijun Zhan
2020	—	`conf`	Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. CDC Bai Xue, Naijun Zhan, Martin Fränzle
2020	—	`conf`	Learning One-Clock Timed Automata. TACAS (1) Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
2020	—	`conf`	Nonlinear Craig Interpolant Generation. CAV (1) Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai
2020	C	`conf`	PAC Learning of Deterministic One-Clock Timed Automata. ICFEM Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan
2020	Misc	`conf`	Probably Approximately Correct Interpolants Generation. SETTA Bai Xue, Naijun Zhan
2020	J	`jnl`	Safety Verification for Random Ordinary Differential Equations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, Bican Xia
2020	—	`conf`	Unbounded-Time Safety Verification of Stochastic Differential Dynamics. CAV (2) Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan
2019	—	`conf`	ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ARCH@CPSIoTWeek Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
2019	J	`jnl`	Editorial. Formal Aspects Comput. Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan
2019	—	`conf`	Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. CAV (2) Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
2019	J	`jnl`	Learning One-Clock Timed Automata. CoRR Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
2019	A	`conf`	NIL: Learning Nonlinear Interpolants. CADE Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
2019	J	`jnl`	NIL: Learning Nonlinear Interpolants. CoRR Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
2019	J	`jnl`	Nonlinear Craig Interpolant Generation. CoRR Ting Gan, Bican Xia, Bai Xue, Naijun Zhan
2019	C	`conf`	Probably Approximate Safety Verification of Hybrid Dynamical Systems. ICFEM Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran
2019	C	`ed.`	Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019, La Jolla, CA, USA, October 9-11, 2019. MEMOCODE Partha S. Roop, Naijun Zhan, Sicun Gao, Pierluigi Nuzzo
2019	J	`jnl`	Quantum Hoare Logic. Arch. Formal Proofs Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
2019	—	`conf`	Robust invariant sets generation for state-constrained perturbed polynomial systems. HSCC Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle
2019	J	`jnl`	Synthesizing More Expressive Invariants by Semidefinite Programming. CoRR Qiuye Wang, Lihong Zhi, Naijun Zhan, Bai Xue, Zhi-Hong Yang
2019	—	`conf`	Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. CAV (1) Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, Bai Xue
2019	—	`conf`	Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. UTP Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan
2018	—	`conf`	ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan
2018	—	`ch.`	Decidability of the Initial-State Opacity of Real-Time Automata. Symposium on Real-Time and Hybrid Systems Lingtai Wang, Naijun Zhan
2018	—	`conf`	Model Checking Bounded Continuous-time Extended Linear Duration Invariants. HSCC Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi
2018	—	`conf`	Monitoring CTMCs by Multi-clock Timed Automata. CAV (1) Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan
2018	J	`jnl`	Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations. CoRR Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan
2018	J	`jnl`	Parameter Synthesis Problems for one parametric clock Timed Automata. CoRR Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen
2018	J	`jnl`	Reachability Analysis for Solvable Dynamical Systems. IEEE Trans. Autom. Control. Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan
2018	J	`jnl`	Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems. CoRR Bai Xue, Naijun Zhan
2018	Misc	`conf`	Robust Non-termination Analysis of Numerical Software. SETTA Bai Xue, Naijun Zhan, Yangjia Li, Qiuye Wang
2018	—	`book`	Symposium on Real-Time and Hybrid Systems - Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday Symposium on Real-Time and Hybrid Systems Cliff B. Jones, Ji Wang, Naijun Zhan
2018	J	`jnl`	Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. CoRR Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She
2018	J	`jnl`	The Opacity of Real-Time Automata. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Lingtai Wang, Naijun Zhan, Jie An
2018	—	`conf`	Under-Approximating Reach Sets for Polynomial Continuous Systems. HSCC Bai Xue, Martin Fränzle, Naijun Zhan
2018	B	`conf`	What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. ATVA Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
2017	J	`jnl`	A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. Formal Aspects Comput. Shuling Wang, Naijun Zhan, Lijun Zhang
2017	J	`jnl`	Barrier certificates revisited. J. Symb. Comput. Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan
2017	Misc	`conf`	Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. SETTA Dimitar P. Guelev, Shuling Wang, Naijun Zhan
2017	J	`jnl`	Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus. CoRR Dimitar P. Guelev, Shuling Wang, Naijun Zhan
2017	B	`conf`	Finding Polynomial Loop Invariants for Probabilistic Programs. ATVA Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
2017	J	`jnl`	Finding polynomial loop invariants for probabilistic programs. CoRR Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
2017	—	`book`	Formal Verification of Simulink/Stateflow Diagrams, A Deductive Approach. Naijun Zhan, Shuling Wang, Hengjun Zhao
2017	J	`jnl`	Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. J. Syst. Sci. Complex. Qiuye Wang, Yangjia Li, Bican Xia, Naijun Zhan
2017	—	`ch.`	MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. Provably Correct Systems Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, Liang Zou
2017	J	`jnl`	Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. Comput. J. Shuling Wang, Flemming Nielson, Hanne Riis Nielson, Naijun Zhan
2017	—	`conf`	Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. FORMATS Bai Xue, Peter Nazier Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li, Naijun Zhan
2017	B	`conf`	Synthesizing SystemC Code from Delay Hybrid CSP. APLAS Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan
2017	J	`jnl`	Synthesizing SystemC Code from Delay Hybrid CSP. CoRR Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan
2016	J	`jnl`	A Theorem Prover for Quantum Hoare Logic and Its Applications. CoRR Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan
2016	—	`conf`	A Two-Way Path Between Formal and Informal Design of Embedded Systems. UTP Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, Naijun Zhan
2016	B	`conf`	Approximate Bisimulation and Discretization of Hybrid CSP. FM Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan
2016	J	`jnl`	Approximate Bisimulation and Discretization of Hybrid CSP. CoRR Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan
2016	—	`conf`	Computing reachable sets of linear vector fields revisited. ECC Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan
2016	Misc	`ed.`	Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings SETTA Martin Fränzle, Deepak Kapur, Naijun Zhan
2016	A	`conf`	Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. IJCAR Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen
2016	J	`jnl`	Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}. CoRR Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen
2016	B	`conf`	Validated Simulation-Based Verification of Delayed Differential Dynamics. FM Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
2015	B	`conf`	Abstraction of Elementary Hybrid Systems by Variable Transformation. FM Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou
2015	C	`conf`	An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. ICFEM Shuling Wang, Naijun Zhan, Liang Zou
2015	—	`conf`	Automatic Verification of Stability and Safety for Delay Differential Equations. CAV (2) Liang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad
2015	J	`jnl`	Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. Sci. China Inf. Sci. Ehsan Ahmad, Yunwei Dong, Brian R. Larson, Jidong Lü, Tao Tang, Naijun Zhan
2015	B	`conf`	Decidability of the Reachability for a Family of Linear Vector Fields. ATVA Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan
2015	Misc	`conf`	Extending Hybrid CSP with Probability and Stochasticity. SETTA Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang
2015	J	`jnl`	Extending Hybrid CSP with Probability and Stochasticity. CoRR Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang
2015	B	`conf`	Formal Verification of Simulink/Stateflow Diagrams. ATVA Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle
2015	J	`jnl`	Termination Analysis of Polynomial Programs with Equality Conditions. CoRR Yangjia Li, Hui Lu, Naijun Zhan, Mingshuai Chen, Guohua Wu
2014	J	`jnl`	Abstraction of Elementary Hybrid Systems by Variable Transformation. CoRR Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou
2014	—	`conf`	Adding Formal Meanings to AADL with Hybrid Annex. FACS Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan, Liang Zou
2014	—	`conf`	Combining Formal and Informal Methods in the Design of Spacecrafts. SETSS Mengfei Yang, Naijun Zhan
2014	J	`jnl`	Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. Jiang Liu, Ming Xu, Naijun Zhan, Hengjun Zhao
2014	B	`conf`	Formal Verification of a Descent Guidance Control Program of a Lunar Lander. FM Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen
2014	—	`conf`	Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. HILT Ehsan Ahmad, Brian R. Larson, Stephen C. Barrett, Naijun Zhan, Yunwei Dong
2013	C	`conf`	An Interface Model of Software Components. ICTAC Ruzhen Dong, Naijun Zhan, Liang Zhao
2013	J	`jnl`	Barrier Certificates Revisited. CoRR Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan
2013	—	`conf`	Bounded model-checking of discrete duration calculus. HSCC Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan
2013	B	`conf`	CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. ATVA Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang
2013	—	`conf`	Formal Modelling, Analysis and Verification of Hybrid Systems. ICTAC Training School on Software Engineering Naijun Zhan, Shuling Wang, Hengjun Zhao
2013	J	`jnl`	Generating Non-Linear Interpolants by Semidefinite Programming CoRR Liyun Dai, Bican Xia, Naijun Zhan
2013	A*	`conf`	Generating Non-linear Interpolants by Semidefinite Programming. CAV Liyun Dai, Bican Xia, Naijun Zhan
2013	J	`jnl`	Model checking conditional CSL for continuous-time Markov chains. Inf. Process. Lett. Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang
2013	—	`conf`	Super-Dense Computation in Verification of Hybrid CSP Processes. FACS Dimitar P. Guelev, Shuling Wang, Naijun Zhan, Chaochen Zhou
2013	J	`jnl`	Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation CoRR Deepak Kapur, Naijun Zhan, Hengjun Zhao
2013	—	`conf`	Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants. Theories of Programming and Formal Methods Hengjun Zhao, Naijun Zhan, Deepak Kapur
2013	—	`conf`	Towards a Failure Model of Software Components. FACS Ruzhen Dong, Naijun Zhan
2013	—	`conf`	Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving. VSTTE Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, Yu Liu
2013	Misc	`conf`	Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. EMSOFT Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle, Shengchao Qin
2012	J	`jnl`	A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example CoRR Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen
2012	B	`conf`	A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. FM Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen
2012	C	`conf`	An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. TAMC Shuling Wang, Naijun Zhan, Dimitar P. Guelev
2012	J	`jnl`	Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems. Math. Comput. Sci. Jiang Liu, Naijun Zhan, Hengjun Zhao
2012	—	`conf`	Unblockable compositions of software components. CBSE Ruzhen Dong, Johannes Faber, Zhiming Liu, Jirí Srba, Naijun Zhan, Jiaqi Zhu
2011	J	`jnl`	A Complete Method to Polynomial Differential Invariant Generation for Hybrid Systems CoRR Jiang Liu, Naijun Zhan, Hengjun Zhao
2011	J	`jnl`	Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems CoRR Jiang Liu, Naijun Zhan, Hengjun Zhao
2011	Misc	`conf`	Computing semi-algebraic invariants for polynomial dynamical systems. EMSOFT Jiang Liu, Naijun Zhan, Hengjun Zhao
2011	J	`jnl`	Symbolic decision procedure for termination of linear programs. Formal Aspects Comput. Bican Xia, Lu Yang, Naijun Zhan, Zhihai Zhang
2010	B	`conf`	A Calculus for Hybrid CSP. APLAS Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, Liang Zou
2010	J	`jnl`	Connection between logical and algebraic approaches to concurrent systems. Math. Struct. Comput. Sci. Naijun Zhan
2010	J	`jnl`	On hierarchically developing reactive systems. Inf. Comput. Naijun Zhan, Mila E. Majster-Cederbaum
2010	J	`jnl`	Rate monotonic scheduling re-analysed. Inf. Process. Lett. Qiwen Xu, Naijun Zhan
2010	J	`jnl`	Recent advances in program verification through computer algebra. Frontiers Comput. Sci. China Lu Yang, Chaochen Zhou, Naijun Zhan, Bican Xia
2010	Misc	`conf`	Refinement of models of software components. SAC Zizhen Wang, Hanpin Wang, Naijun Zhan
2009	—	`conf`	Model Checking Linear Duration Invariants of Networks of Automata. FSEN Miaomiao Zhang, Zhiming Liu, Naijun Zhan
2009	J	`jnl`	Refinement and verification in component-based model-driven design. Sci. Comput. Program. Zhenbang Chen, Zhiming Liu, Anders P. Ravn, Volker Stolz, Naijun Zhan
2008	J	`jnl`	Basic research in computer science and software engineering at SKLCS. Frontiers Comput. Sci. China Jian Zhang, Wenhui Zhang, Naijun Zhan, Yi-Dong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang, Enhua Wu, Hongan Wang, Xueyang Zhu
2008	—	`conf`	Component Publications and Compositions. UTP Naijun Zhan, Eun-Young Kang, Zhiming Liu
2008	J	`jnl`	Formalising Scheduling Theories in Duration Calculus. Nord. J. Comput. Qiwen Xu, Naijun Zhan
2008	C	`conf`	Program Verification by Reduction to Semi-algebraic Systems Solving. ISoLA Bican Xia, Lu Yang, Naijun Zhan
2007	—	`conf`	A Model of Component-Based Programming. FSEN Xin Chen, Jifeng He, Zhiming Liu, Naijun Zhan
2007	C	`conf`	Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. ICTAC Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou
2007	—	`conf`	Generating Polynomial Invariants with DISCOVERER and QEPCAD. Formal Methods and Hybrid Real-Time Systems Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan
2007	—	`conf`	Modelling with Relational Calculus of Object and Component Systems - rCOS. CoCoME Zhenbang Chen, Abdelhakim Hannousse, Dang Van Hung, Istvan Knoll, Xiaoshan Li, Zhiming Liu, Yang Liu, Qu Nan, Joseph C. Okika, Anders P. Ravn, Volker Stolz, Lu Yang, Naijun Zhan
2006	C	`conf`	Connecting Algebraic and Logical Descriptions of Concurrent Systems. ISoLA Naijun Zhan
2005	C	`conf`	Compositionality of Fixpoint Logic with Chop. ICTAC Naijun Zhan, Jinzhao Wu
2005	C	`conf`	Deriving Non-determinism from Conjunction and Disjunction. FORTE Naijun Zhan, Mila E. Majster-Cederbaum
2005	—	`conf`	Program Verification by Using DISCOVERER. VSTTE Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou
2004	C	`conf`	Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. ICFEM Mila E. Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan
2003	B	`conf`	Action Refinement from a Logical Point of View. VMCAI Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher
2003	—	`conf`	Combining Hierarchical Specification with Hierarchical Implementation. ASIAN Naijun Zhan
2003	—	`conf`	Compositional Properties of Sequential Processes. SVV@ICLP Naijun Zhan
2001	J	`jnl`	An Intuitive Formal Proof for Deadline Driven Scheduler. J. Comput. Sci. Technol. Naijun Zhan
2001	C	`conf`	Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol. APSEC Huadong Ma, Liang Li, Jianzhong Wang, Naijun Zhan
2000	B	`conf`	Another formal proof for Deadline Driven Scheduler. RTCSA Naijun Zhan
2000	B	`conf`	Completeness of Higher-Order Duration Calculus. CSL Naijun Zhan
1999	B	`conf`	A Formal Proof of the Rate Monotonic Scheduler. RTCSA Shuzhen Dong, Qiwen Xu, Naijun Zhan