| 2026 | AAAI | RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation. | Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan |
| 2026 | FM | Exact Moment Estimation of Stochastic Differential Dynamics. | Shenghua Feng, Jie An, Naijun Zhan, Fanjiang Xu |
| 2026 | FM | Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel. | Tianqi Zhao, Qinxiang Cao, Shenghua Feng, Minghui Zhou, Naijun Zhan, Yongzhi Cao, Junfeng Zhao, Haiyan Zhao, Hao Wang, Zhenjiang Hu |
| 2026 | IJCAR | A Complete Proof System for HyperLTL. | Naijun Zhan, Wen Tang, Dimitar P. Guelev |
| 2026 | TACAS | Quantifier Elimination Meets Treewidth. | Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan |
| 2026 | TASE | QCP: A Practical Separation Logic-Based C Program Verification Tool. | Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Zihan Zhang, Juanru Li, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao |
| 2025 | ACL | Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. | Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiao-hong Chen, Naijun Zhan |
| 2025 | MEMOCODE | Formal Design of Safety-critical Embedded Systems. | Naijun Zhan |
| 2025 | RTSS | On Synthesis of Timed Regular Expressions. | Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang |
| 2025 | SETTA | HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. | Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan |
| 2025 | SETTA | Efficient Decomposition Identification of Deterministic Finite Automata from Examples. | Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang |
| 2024 | FM | The Opacity of Timed Automata. | Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo |
| 2024 | FM | Switching Controller Synthesis for Hybrid Systems Against STL Formulas. | Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan |
| 2024 | FM | On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. | Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan |
| 2024 | FM | Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. | Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan |
| 2024 | RTCSA | Improving the Reaction Latency Analysis of Message Synchronization in ROS. | Chenhao Wu, Ruoxiang Li, Naijun Zhan, Nan Guan |
| 2024 | SETTA | Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation. | Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju |
| 2024 | SETTA | The Design of Intelligent Temperature Control System of Smart House with MARS. | Yihao Yin, Hao Wu, Shuling Wang, Xiong Xu, Fanjiang Xu, Naijun Zhan |
| 2022 | ATVA | Learning Deterministic One-Clock Timed Automata via Mutation Testing. | Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan |
| 2022 | ICFEM | Machine-Checked Executable Semantics of Stateflow. | Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan |
| 2021 | CAV | Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. | Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen |
| 2021 | RTAS | Brief Industry Paper: 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, Naijun Zhan |
| 2021 | SETTA | Formal Analysis of 5G AKMA. | Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao |
| 2020 | CAV | Unbounded-Time Safety Verification of Stochastic Differential Dynamics. | Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan |
| 2020 | CAV | Nonlinear Craig Interpolant Generation. | Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai |
| 2020 | ICFEM | PAC Learning of Deterministic One-Clock Timed Automata. | Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan |
| 2020 | SETTA | Probably Approximately Correct Interpolants Generation. | Bai Xue, Naijun Zhan |
| 2020 | TACAS | Learning One-Clock Timed Automata. | Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang |
| 2019 | CADE | NIL: Learning Nonlinear Interpolants. | Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan |
| 2019 | CAV | Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. | Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Frnzle, Bai Xue |
| 2019 | CAV | Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. | Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan |
| 2019 | ICFEM | Probably Approximate Safety Verification of Hybrid Dynamical Systems. | Bai Xue, Martin Frnzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran |
| 2018 | ATVA | What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. | Mingshuai Chen, Martin Frnzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan |
| 2018 | CAV | Monitoring CTMCs by Multi-clock Timed Automata. | Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan |
| 2018 | SETTA | Robust Non-termination Analysis of Numerical Software. | Bai Xue, Naijun Zhan, Yangjia Li, Qiuye Wang |
| 2017 | APLAS | Synthesizing SystemC Code from Delay Hybrid CSP. | Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan |
| 2017 | ATVA | Finding Polynomial Loop Invariants for Probabilistic Programs. | Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia |
| 2017 | SETTA | Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. | Dimitar P. Guelev, Shuling Wang, Naijun Zhan |
| 2016 | CADE | Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. | Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
| 2016 | FM | Validated Simulation-Based Verification of Delayed Differential Dynamics. | Mingshuai Chen, Martin Frnzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan |
| 2016 | FM | Approximate Bisimulation and Discretization of Hybrid CSP. | Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan |
| 2015 | ATVA | Decidability of the Reachability for a Family of Linear Vector Fields. | Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan |
| 2015 | ATVA | Formal Verification of Simulink/Stateflow Diagrams. | Liang Zou, Naijun Zhan, Shuling Wang, Martin Frnzle |
| 2015 | CAV | Automatic Verification of Stability and Safety for Delay Differential Equations. | Liang Zou, Martin Frnzle, Naijun Zhan, Peter Nazier Mosaad |
| 2015 | FM | Abstraction of Elementary Hybrid Systems by Variable Transformation. | Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou |
| 2015 | ICFEM | An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. | Shuling Wang, Naijun Zhan, Liang Zou |
| 2015 | SETTA | Extending Hybrid CSP with Probability and Stochasticity. | Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang |
| 2014 | FM | Formal Verification of a Descent Guidance Control Program of a Lunar Lander. | Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen |
| 2013 | ATVA | CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. | Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang |
| 2013 | CAV | Generating Non-linear Interpolants by Semidefinite Programming. | Liyun Dai, Bican Xia, Naijun Zhan |
| 2013 | EMSOFT | Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. | Liang Zou, Naijun Zhan, Shuling Wang, Martin Frnzle, Shengchao Qin |
| 2013 | ICTAC | An Interface Model of Software Components. | Ruzhen Dong, Naijun Zhan, Liang Zhao |
| 2013 | ICTAC | Formal Modelling, Analysis and Verification of Hybrid Systems. | Naijun Zhan, Shuling Wang, Hengjun Zhao |
| 2012 | FM | 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, Kim G. Larsen |
| 2012 | TAMC | An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. | Shuling Wang, Naijun Zhan, Dimitar P. Guelev |
| 2011 | EMSOFT | Computing semi-algebraic invariants for polynomial dynamical systems. | Jiang Liu, Naijun Zhan, Hengjun Zhao |
| 2010 | APLAS | A Calculus for Hybrid CSP. | Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, Liang Zou |
| 2010 | SAC | Refinement of models of software components. | Zizhen Wang, Hanpin Wang, Naijun Zhan |
| 2008 | ISoLA | Program Verification by Reduction to Semi-algebraic Systems Solving. | Bican Xia, Lu Yang, Naijun Zhan |
| 2007 | ICTAC | Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. | Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou |
| 2006 | ISoLA | Connecting Algebraic and Logical Descriptions of Concurrent Systems. | Naijun Zhan |
| 2005 | FORTE | Deriving Non-determinism from Conjunction and Disjunction. | Naijun Zhan, Mila E. Majster-Cederbaum |
| 2005 | ICTAC | Compositionality of Fixpoint Logic with Chop. | Naijun Zhan, Jinzhao Wu |
| 2004 | ICFEM | Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. | Mila E. Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan |
| 2003 | VMCAI | Action Refinement from a Logical Point of View. | Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher |
| 2001 | APSEC | Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol. | Huadong Ma, Liang Li, Jianzhong Wang, Naijun Zhan |
| 2000 | CSL | Completeness of Higher-Order Duration Calculus. | Naijun Zhan |
| 2000 | RTCSA | Another formal proof for Deadline Driven Scheduler. | Naijun Zhan |
| 1999 | RTCSA | A Formal Proof of the Rate Monotonic Scheduler. | Shuzhen Dong, Qiwen Xu, Naijun Zhan |