default search action
Naijun Zhan
Person information
- affiliation: Chinese Academy of Sciences, State Key Laboratory of Computer Science, Beijing, China
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j46]Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, Naijun Zhan:
A decision procedure for string constraints with string/integer conversion and flat regular constraints. Acta Informatica 61(1): 23-52 (2024) - [j45]Bai Xue
, Naijun Zhan
Reach-Avoid Verification Based on Convex Optimization. IEEE Trans. Autom. Control. 69(1): 598-605 (2024) - [j44]Bai Xue
Reach-Avoid Analysis for Polynomial Stochastic Differential Equations. IEEE Trans. Autom. Control. 69(3): 1882-1889 (2024) - [j43]Chenhao Wu
Modeling and Analysis of the LatestTime Message Synchronization Policy in ROS. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 43(11): 3576-3587 (2024) - [c92]Hao Wu
Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. FM (1) 2024: 92-110 - [c91]Han Su
Switching Controller Synthesis for Hybrid Systems Against STL Formulas. FM (2) 2024: 229-247 - [c90]Hao Wu
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. FM (2) 2024: 248-266 - [c89]Jie An
The Opacity of Timed Automata. FM (1) 2024: 620-637 - [c88]Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao, Naijun Zhan:
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. ICCPS 2024: 123-134 - [c87]Chenhao Wu, Ruoxiang Li, Naijun Zhan, Nan Guan:
Improving the Reaction Latency Analysis of Message Synchronization in ROS. RTCSA 2024: 43-48 - [c86]Yihao Yin, Hao Wu, Shuling Wang, Xiong Xu, Fanjiang Xu, Naijun Zhan:
The Design of Intelligent Temperature Control System of Smart House with MARS. SETTA 2024: 217-235 - [c85]Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju:
Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation. SETTA 2024: 256-274 - [i42]Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan:
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. CoRR abs/2402.15674 (2024) - [i41]Bohua Zhan, Xiong Xu, Qiang Gao, Zekun Ji, Xiangyu Jin, Shuling Wang, Naijun Zhan:
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. CoRR abs/2403.03035 (2024) - [i40]Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, Shiyang Wu:
Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. CoRR abs/2403.17567 (2024) - [i39]Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan:
Switching Controller Synthesis for Hybrid Systems Against STL Formulas. CoRR abs/2406.16588 (2024) - [i38]Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan:
Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets. CoRR abs/2407.00625 (2024) - [i37]Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan:
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. CoRR abs/2407.08936 (2024) - 2023
- [j42]Wenyou Liu, Yunjun Bai, Li Jiao, Naijun Zhan:
Safety guarantee for time-delay systems with disturbances. Sci. China Inf. Sci. 66(3) (2023) - [j41]Marieke Huisman
Introduction to the Special Section on FM 2021. Formal Aspects Comput. 35(2): 6:1-6:2 (2023) - [j40]Xiong Xu
A denotational semantics of Simulink with higher-order UTP. J. Log. Algebraic Methods Program. 130: 100809 (2023) - [j39]Shenghua Feng
Lower Bounds for Possibly Divergent Probabilistic Programs. Proc. ACM Program. Lang. 7(OOPSLA1): 696-726 (2023) - [j38]Xiong Xu
Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. ACM Trans. Softw. Eng. Methodol. 32(1): 9:1-9:48 (2023) - [i36]Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan:
Lower Bounds for Possibly Divergent Probabilistic Programs. CoRR abs/2302.06082 (2023) - [i35]Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin:
A Generalized Hybrid Hoare Logic. CoRR abs/2303.15020 (2023) - [i34]Jiang Liu, Han Su, Yunjun Bai, Bin Gu, Bai Xue, Mengfei Yang, Naijun Zhan:
Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. CoRR abs/2309.05906 (2023) - [i33]Han Su, Jiyu Zhu, Shenghua Feng, Yunjun Bai, Bin Gu, Jiang Liu, Mengfei Yang, Naijun Zhan:
Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. CoRR abs/2309.05908 (2023) - [i32]Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhi-Hong Yang:
Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. CoRR abs/2310.11133 (2023) - [i31]Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan:
Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. CoRR abs/2312.15416 (2023) - 2022
- [j37]Marieke Huisman
Preface for the formal methods in system design special issue on 'Formal Methods 2021'. Formal Methods Syst. Des. 61(1): 1-2 (2022) - [j36]Qiuye Wang, Mingshuai Chen
Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. Inf. Comput. 289(Part): 104965 (2022) - [j35]Tengshun Yang
Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). J. Syst. Archit. 126: 102478 (2022) - [j34]Bai Xue
Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. IEEE Trans. Autom. Control. 67(2): 1053-1060 (2022) - [j33]Xiong Xu
Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theor. Comput. Sci. 903: 1-25 (2022) - [c84]Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng:
Differential Games Based on Invariant Sets Generation. ACC 2022: 1285-1292 - [c83]Xiaochen Tang
Learning Deterministic One-Clock Timed Automata via Mutation Testing. ATVA 2022: 233-248 - [c82]Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan:
Machine-Checked Executable Semantics of Stateflow. ICFEM 2022: 421-438 - [i30]Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan:
Defensive Design of Saturating Counters Based on Differential Privacy. CoRR abs/2206.00279 (2022) - [i29]Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan:
Machine-checked executable semantics of Stateflow. CoRR abs/2207.11965 (2022) - [i28]Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu:
Reach-avoid Verification Based on Convex Optimization. CoRR abs/2208.08105 (2022) - [i27]Bai Xue, Naijun Zhan, Martin Fränzle:
Reach-Avoid Analysis for Stochastic Differential Equations. CoRR abs/2208.10752 (2022) - [i26]Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen:
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming. CoRR abs/2209.09703 (2022) - 2021
- [j32]Mingshuai Chen
Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control. Acta Informatica 58(5): 497-528 (2021) - [j31]Jie An
Learning real-time automata. Sci. China Inf. Sci. 64(9) (2021) - [j30]Xiangyu Jin, Jie An
Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. 33(3): 385-406 (2021) - [j29]Arvind Easwaran, Qi Zhu, Naijun Zhan:
Special issue on design of embedded software and systems (SI: ICESS19). J. Syst. Archit. 116: 101973 (2021) - [j28]Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. SIAM J. Control. Optim. 59(2): 1083-1108 (2021) - [j27]Bai Xue
Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. IEEE Trans. Autom. Control. 66(1): 283-290 (2021) - [j26]Jie An
Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. 20(5s): 99:1-99:26 (2021) - [c81]Bai Xue, Renjue Li, Naijun Zhan, Martin Fränzle
Reach-avoid Analysis for Stochastic Discrete-time Systems. ACC 2021: 4879-4885 - [c80]Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan:
ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS 2021: 120-132 - [c79]Qiuye Wang
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CAV (1) 2021: 443-466 - [c78]Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu, Li Jiao:
Reach-Avoid Analysis for Delay Differential Equations. CDC 2021: 1301-1307 - [c77]Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan:
Switching controller synthesis for delay hybrid systems under perturbations. HSCC 2021: 3:1-3:11 - [c76]Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan:
Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. RTAS 2021: 457-460 - [c75]Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao:
Formal Analysis of 5G AKMA. SETTA 2021: 102-121 - [e5]Marieke Huisman
Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0 [contents] - [i25]Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan:
Switching Controller Synthesis for Delay Hybrid Systems under Perturbations. CoRR abs/2103.11565 (2021) - [i24]Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen:
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CoRR abs/2105.14311 (2021) - 2020
- [j25]Jian Wang, Jie An
From model to implementation: a network algorithm programming language. Sci. China Inf. Sci. 63(7) (2020) - [j24]Bai Xue
Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. IEEE Trans. Autom. Control. 65(4): 1468-1483 (2020) - [j23]Bai Xue
Safety Verification for Random Ordinary Differential Equations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11): 4090-4101 (2020) - [j22]Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, Naijun Zhan:
Automatically Generating SystemC Code from HCSP Formal Models. ACM Trans. Softw. Eng. Methodol. 29(1): 4:1-4:39 (2020) - [c74]Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan:
ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. ARCH 2020: 153-174 - [c73]Shenghua Feng
Unbounded-Time Safety Verification of Stochastic Differential Dynamics. CAV (2) 2020: 327-348 - [c72]Ting Gan
Nonlinear Craig Interpolant Generation. CAV (1) 2020: 415-438 - [c71]Bai Xue, Naijun Zhan, Martin Fränzle
Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. CDC 2020: 867-873 - [c70]Wei Shen
PAC Learning of Deterministic One-Clock Timed Automata. ICFEM 2020: 129-146 - [c69]Bai Xue, Naijun Zhan:
Probably Approximately Correct Interpolants Generation. SETTA 2020: 143-159 - [c68]Jie An
Learning One-Clock Timed Automata. TACAS (1) 2020: 444-462
2010 – 2019
- 2019
- [j21]Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan:
Quantum Hoare Logic. Arch. Formal Proofs 2019 (2019) - [j20]Martin Fränzle
Editorial. Formal Aspects Comput. 31(1): 1 (2019) - [c67]Mingshuai Chen
NIL: Learning Nonlinear Interpolants. CADE 2019: 178-196 - [c66]Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. CAV (2) 2019: 187-207 - [c65]Shenghua Feng
Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. CAV (1) 2019: 650-669 - [c64]Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan:
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ARCH@CPSIoTWeek 2019: 141-161 - [c63]Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle:
Robust invariant sets generation for state-constrained perturbed polynomial systems. HSCC 2019: 128-137 - [c62]Bai Xue, Martin Fränzle
Probably Approximate Safety Verification of Hybrid Dynamical Systems. ICFEM 2019: 236-252 - [c61]Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan:
Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. UTP 2019: 109-129 - [e4]Partha S. Roop, Naijun Zhan, Sicun Gao, Pierluigi Nuzzo:
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. ACM 2019, ISBN 978-1-4503-6997-8 [contents] - [i23]Ting Gan, Bican Xia, Bai Xue, Naijun Zhan:
Nonlinear Craig Interpolant Generation. CoRR abs/1903.01297 (2019) - [i22]Qiuye Wang, Lihong Zhi, Naijun Zhan, Bai Xue, Zhi-Hong Yang:
Synthesizing More Expressive Invariants by Semidefinite Programming. CoRR abs/1903.04668 (2019) - [i21]Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan:
NIL: Learning Nonlinear Interpolants. CoRR abs/1905.11625 (2019) - [i20]Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang:
Learning One-Clock Timed Automata. CoRR abs/1910.10680 (2019) - 2018
- [j19]Ting Gan
Reachability Analysis for Solvable Dynamical Systems. IEEE Trans. Autom. Control. 63(7): 2003-2018 (2018) - [j18]Lingtai Wang, Naijun Zhan
The Opacity of Real-Time Automata. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11): 2845-2856 (2018) - [c60]Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan:
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS 2018: 110-127 - [c59]Mingshuai Chen
What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. ATVA 2018: 56-74 - [c58]Yijun Feng, Joost-Pieter Katoen
Monitoring CTMCs by Multi-clock Timed Automata. CAV (1) 2018: 507-526 - [c57]Bai Xue, Martin Fränzle, Naijun Zhan:
Under-Approximating Reach Sets for Polynomial Continuous Systems. HSCC 2018: 51-60 - [c56]Jie An
Model Checking Bounded Continuous-time Extended Linear Duration Invariants. HSCC 2018: 81-90 - [c55]Bai Xue, Naijun Zhan, Yangjia Li, Qiuye Wang:
Robust Non-termination Analysis of Numerical Software. SETTA 2018: 69-88 - [p2]Lingtai Wang, Naijun Zhan:
Decidability of the Initial-State Opacity of Real-Time Automata. Symposium on Real-Time and Hybrid Systems 2018: 44-60 - [e3]Cliff B. Jones, Ji Wang, Naijun Zhan:
Symposium on Real-Time and Hybrid Systems - 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 [contents] - [i19]Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen:
Parameter Synthesis Problems for one parametric clock Timed Automata. CoRR abs/1809.07177 (2018) - [i18]Bai Xue, Naijun Zhan:
Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems. CoRR abs/1811.11454 (2018) - [i17]Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She:
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. CoRR abs/1812.10588 (2018) - [i16]Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan:
Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations. CoRR abs/1812.11718 (2018) - 2017
- [j17]Shuling Wang, Flemming Nielson
Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. Comput. J. 60(8): 1111-1130 (2017) - [j16]Shuling Wang
A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. Formal Aspects Comput. 29(4): 751-775 (2017) - [j15]Qiuye Wang
Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. J. Syst. Sci. Complex. 30(1): 234-252 (2017) - [j14]Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan:
Barrier certificates revisited. J. Symb. Comput. 80: 62-86 (2017) - [c54]Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan:
Synthesizing SystemC Code from Delay Hybrid CSP. APLAS 2017: 21-41 - [c53]Yijun Feng, Lijun Zhang, David N. Jansen
Finding Polynomial Loop Invariants for Probabilistic Programs. ATVA 2017: 400-416 - [c52]Bai Xue, Peter Nazier Mosaad, Martin Fränzle
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. FORMATS 2017: 281-299 - [c51]Dimitar P. Guelev, Shuling Wang, Naijun Zhan:
Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. SETTA 2017: 110-127 - [p1]Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, Liang Zou:
MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. Provably Correct Systems 2017: 39-58 - [e2]Naijun Zhan, Shuling Wang, Hengjun Zhao:
Formal Verification of Simulink/Stateflow Diagrams, A Deductive Approach. Springer 2017, ISBN 978-3-319-47014-6 - [i15]Dimitar P. Guelev, Shuling Wang, Naijun Zhan:
Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus. CoRR abs/1706.06246 (2017) - [i14]Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia:
Finding polynomial loop invariants for probabilistic programs. CoRR abs/1707.02690 (2017) - [i13]Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan:
Synthesizing SystemC Code from Delay Hybrid CSP. CoRR abs/1709.09019 (2017) - 2016
- [c50]Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen:
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. IJCAR 2016: 195-212 - [c49]Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan:
Computing reachable sets of linear vector fields revisited. ECC 2016: 419-426 - [c48]Mingshuai Chen, Martin Fränzle
Validated Simulation-Based Verification of Delayed Differential Dynamics. FM 2016: 137-154 - [c47]Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan:
Approximate Bisimulation and Discretization of Hybrid CSP. FM 2016: 702-720 - [c46]Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, Naijun Zhan:
A Two-Way Path Between Formal and Informal Design of Embedded Systems. UTP 2016: 65-92 - [e1]Martin Fränzle
Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science 9984, 2016, ISBN 978-3-319-47676-6 [contents] - [i12]Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan:
A Theorem Prover for Quantum Hoare Logic and Its Applications. CoRR abs/1601.03835 (2016) - [i11]Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen:
Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}. CoRR abs/1601.04802 (2016) - [i10]Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan:
Approximate Bisimulation and Discretization of Hybrid CSP. CoRR abs/1609.00091 (2016) - 2015
- [j13]Ehsan Ahmad
Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. Sci. China Inf. Sci. 58(11): 1-20 (2015) - [c45]Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle
Formal Verification of Simulink/Stateflow Diagrams. ATVA 2015: 464-481 - [c44]Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan:
Decidability of the Reachability for a Family of Linear Vector Fields. ATVA 2015: 482-499 - [c43]Liang Zou, Martin Fränzle
Automatic Verification of Stability and Safety for Delay Differential Equations. CAV (2) 2015: 338-355 - [c42]Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou:
Abstraction of Elementary Hybrid Systems by Variable Transformation. FM 2015: 360-377 - [c41]Shuling Wang, Naijun Zhan, Liang Zou:
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. ICFEM 2015: 382-399 - [c40]Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang:
Extending Hybrid CSP with Probability and Stochasticity. SETTA 2015: 87-102 - [i9]Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang:
Extending Hybrid CSP with Probability and Stochasticity. CoRR abs/1509.01660 (2015) - [i8]Yangjia Li, Hui Lu, Naijun Zhan, Mingshuai Chen, Guohua Wu:
Termination Analysis of Polynomial Programs with Equality Conditions. CoRR abs/1510.05201 (2015) - 2014
- [j12]Jiang Liu, Ming Xu, Naijun Zhan, Hengjun Zhao:
Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. 27(6): 1286-1304 (2014) - [c39]Ehsan Ahmad
Adding Formal Meanings to AADL with Hybrid Annex. FACS 2014: 228-247 - [c38]Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen:
Formal Verification of a Descent Guidance Control Program of a Lunar Lander. FM 2014: 733-748 - [c37]Mengfei Yang, Naijun Zhan:
Combining Formal and Informal Methods in the Design of Spacecrafts. SETSS 2014: 290-323 - [c36]Ehsan Ahmad
Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. HILT 2014: 29-38 - [i7]Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou:
Abstraction of Elementary Hybrid Systems by Variable Transformation. CoRR abs/1403.7022 (2014) - 2013
- [j11]Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang:
Model checking conditional CSL for continuous-time Markov chains. Inf. Process. Lett. 113(1-2): 44-50 (2013) - [c35]Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang:
CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. ATVA 2013: 464-468 - [c34]Hengjun Zhao, Naijun Zhan, Deepak Kapur:
Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants. Theories of Programming and Formal Methods 2013: 354-373 - [c33]Liyun Dai, Bican Xia, Naijun Zhan:
Generating Non-linear Interpolants by Semidefinite Programming. CAV 2013: 364-380 - [c32]Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle, Shengchao Qin
Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. EMSOFT 2013: 9:1-9:10 - [c31]Dimitar P. Guelev, Shuling Wang, Naijun Zhan, Chaochen Zhou:
Super-Dense Computation in Verification of Hybrid CSP Processes. FACS 2013: 13-22 - [c30]Ruzhen Dong, Naijun Zhan:
Towards a Failure Model of Software Components. FACS 2013: 119-136 - [c29]Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan:
Bounded model-checking of discrete duration calculus. HSCC 2013: 213-222 - [c28]Ruzhen Dong, Naijun Zhan, Liang Zhao:
An Interface Model of Software Components. ICTAC 2013: 159-176 - [c27]Naijun Zhan, Shuling Wang, Hengjun Zhao:
Formal Modelling, Analysis and Verification of Hybrid Systems. ICTAC Training School on Software Engineering 2013: 207-281 - [c26]Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, Yu Liu:
Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving. VSTTE 2013: 262-280 - [i6]Liyun Dai, Bican Xia, Naijun Zhan:
Generating Non-Linear Interpolants by Semidefinite Programming. CoRR abs/1302.4739 (2013) - [i5]Deepak Kapur, Naijun Zhan, Hengjun Zhao:
Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation. CoRR abs/1304.0825 (2013) - [i4]Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan:
Barrier Certificates Revisited. CoRR abs/1310.6481 (2013) - 2012
- [j10]Jiang Liu, Naijun Zhan, Hengjun Zhao:
Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems. Math. Comput. Sci. 6(4): 395-408 (2012) - [c25]Ruzhen Dong, Johannes Faber, Zhiming Liu, Jirí Srba
Unblockable compositions of software components. CBSE 2012: 103-108 - [c24]Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen
A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. FM 2012: 471-485 - [c23]Shuling Wang, Naijun Zhan, Dimitar P. Guelev:
An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. TAMC 2012: 72-83 - [i3]Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen:
A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. CoRR abs/1203.6025 (2012) - 2011
- [j9]Bican Xia, Lu Yang, Naijun Zhan, Zhihai Zhang:
Symbolic decision procedure for termination of linear programs. Formal Aspects Comput. 23(2): 171-190 (2011) - [c22]Jiang Liu, Naijun Zhan, Hengjun Zhao:
Computing semi-algebraic invariants for polynomial dynamical systems. EMSOFT 2011: 97-106 - [i2]Jiang Liu, Naijun Zhan, Hengjun Zhao:
A Complete Method to Polynomial Differential Invariant Generation for Hybrid Systems. CoRR abs/1102.0705 (2011) - [i1]Jiang Liu, Naijun Zhan, Hengjun Zhao:
Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems. CoRR abs/1103.3372 (2011) - 2010
- [j8]Lu Yang, Chaochen Zhou, Naijun Zhan, Bican Xia:
Recent advances in program verification through computer algebra. Frontiers Comput. Sci. China 4(1): 1-16 (2010) - [j7]Naijun Zhan, Mila E. Majster-Cederbaum:
On hierarchically developing reactive systems. Inf. Comput. 208(9): 997-1019 (2010) - [j6]Qiwen Xu, Naijun Zhan:
Rate monotonic scheduling re-analysed. Inf. Process. Lett. 110(6): 226-231 (2010) - [j5]Naijun Zhan:
Connection between logical and algebraic approaches to concurrent systems. Math. Struct. Comput. Sci. 20(5): 915-950 (2010) - [c21]Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, Liang Zou:
A Calculus for Hybrid CSP. APLAS 2010: 1-15 - [c20]Zizhen Wang, Hanpin Wang, Naijun Zhan:
Refinement of models of software components. SAC 2010: 2311-2318
2000 – 2009
- 2009
- [j4]Zhenbang Chen, Zhiming Liu, Anders P. Ravn, Volker Stolz, Naijun Zhan:
Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4): 168-196 (2009) - [c19]Miaomiao Zhang, Zhiming Liu, Naijun Zhan:
Model Checking Linear Duration Invariants of Networks of Automata. FSEN 2009: 244-259 - 2008
- [j3]Jian Zhang, Wenhui Zhang, Naijun Zhan, Yi-Dong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang, Enhua Wu, Hongan Wang, Xueyang Zhu
Basic research in computer science and software engineering at SKLCS. Frontiers Comput. Sci. China 2(1): 1-11 (2008) - [j2]Qiwen Xu, Naijun Zhan:
Formalising Scheduling Theories in Duration Calculus. Nord. J. Comput. 14(3): 173-201 (2008) - [c18]Bican Xia, Lu Yang, Naijun Zhan:
Program Verification by Reduction to Semi-algebraic Systems Solving. ISoLA 2008: 277-291 - [c17]Naijun Zhan, Eun-Young Kang
Component Publications and Compositions. UTP 2008: 238-257 - 2007
- [c16]Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan:
Generating Polynomial Invariants with DISCOVERER and QEPCAD. Formal Methods and Hybrid Real-Time Systems 2007: 67-82 - [c15]Zhenbang Chen, Abdelhakim Hannousse
Modelling with Relational Calculus of Object and Component Systems - rCOS. CoCoME 2007: 116-145 - [c14]Xin Chen, Jifeng He, Zhiming Liu, Naijun Zhan:
A Model of Component-Based Programming. FSEN 2007: 191-206 - [c13]Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou:
Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. ICTAC 2007: 34-49 - 2006
- [c12]Naijun Zhan:
Connecting Algebraic and Logical Descriptions of Concurrent Systems. ISoLA 2006: 383-391 - 2005
- [c11]Naijun Zhan, Mila E. Majster-Cederbaum:
Deriving Non-determinism from Conjunction and Disjunction. FORTE 2005: 351-365 - [c10]Naijun Zhan, Jinzhao Wu:
Compositionality of Fixpoint Logic with Chop. ICTAC 2005: 136-150 - [c9]Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou:
Program Verification by Using DISCOVERER. VSTTE 2005: 528-538 - 2004
- [c8]Mila E. Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan:
Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. ICFEM 2004: 449-463 - 2003
- [c7]Naijun Zhan:
Combining Hierarchical Specification with Hierarchical Implementation. ASIAN 2003: 110-124 - [c6]Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher:
Action Refinement from a Logical Point of View. VMCAI 2003: 253-267 - [c5]Naijun Zhan:
Compositional Properties of Sequential Processes. SVV@ICLP 2003: 111-128 - 2001
- [j1]Naijun Zhan:
An Intuitive Formal Proof for Deadline Driven Scheduler. J. Comput. Sci. Technol. 16(2): 146-158 (2001) - [c4]Huadong Ma, Liang Li, Jianzhong Wang, Naijun Zhan:
Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol. APSEC 2001: 371- - 2000
- [c3]Naijun Zhan:
Completeness of Higher-Order Duration Calculus. CSL 2000: 442-456 - [c2]Naijun Zhan:
Another formal proof for Deadline Driven Scheduler. RTCSA 2000: 481-485
1990 – 1999
- 1999
- [c1]Shuzhen Dong, Qiwen Xu, Naijun Zhan:
A Formal Proof of the Rate Monotonic Scheduler. RTCSA 1999: 500-
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-13 19:11 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: