Model Checking Bounded Continuous-time Extended Linear Duration Invariants. - Jie An 001; Naijun Zhan; Xiaoshan Li; Miaomiao Zhang 003; Wang Yi 001 (HSCC, 2018)

The Opacity of Real-Time Automata. - Lingtai Wang; Naijun Zhan; Jie An 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

NIL: Learning Nonlinear Interpolants. - Mingshuai Chen; Jian Wang 042; Jie An 001; Bohua Zhan; Deepak Kapur; Naijun Zhan (CADE, 2019)

High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training. - Xiaoxue Hou; Jie An 001; Miaomiao Zhang 003; Bowen Du 002; Jing Liu 012 (ICTAI, 2019)

PAC Learning of Deterministic One-Clock Timed Automata. - Wei Shen; Jie An 001; Bohua Zhan; Miaomiao Zhang 003; Bai Xue 001; Naijun Zhan (ICFEM, 2020)

Learning One-Clock Timed Automata. - Jie An 001; Mingshuai Chen; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (TACAS (1), 2020)

From model to implementation: a network algorithm programming language. - Jian Wang 042; Jie An 001; Mingshuai Chen; Naijun Zhan; Lulin Wang; Miaomiao Zhang 003; Ting Gan (Sci. China Inf. Sci., 2020)

Learning real-time automata. - Jie An 001; Lingtai Wang; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Sci. China Inf. Sci., 2021)

Inferring Switched Nonlinear Dynamical Systems. - Xiangyu Jin; Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Formal Aspects Comput., 2021)

Learning Nondeterministic Real-Time Automata. - Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (ACM Trans. Embed. Comput. Syst., 2021)

Learning Deterministic One-Clock Timed Automata via Mutation Testing. - Xiaochen Tang; Wei Shen; Miaomiao Zhang 003; Jie An 001; Bohua Zhan; Naijun Zhan (ATVA, 2022)

Active Learning of One-Clock Timed Automata Using Constraint Solving. - Runqing Xu; Jie An 001; Bohua Zhan (ATVA, 2022)

Online Causation Monitoring of Signal Temporal Logic. - Zhenya Zhang; Jie An 001; Paolo Arcaini; Ichiro Hasuo (CAV (1), 2023)

Online Causation Monitoring of Signal Temporal Logic (Artifact). - Zhenya Zhang; Jie An 001; Paolo Arcaini; Ichiro Hasuo (Zenodo, 2023)

Online Causation Monitoring of Signal Temporal Logic (Artifact). - Zhenya Zhang; Jie An 001; Paolo Arcaini; Ichiro Hasuo (Zenodo, 2023)

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications. - Sota Sato 001; Jie An 001; Zhenya Zhang; Ichiro Hasuo (CAV (3), 2024)

The Opacity of Timed Automata. - Jie An 001; Qiang Gao; Lingtai Wang; Naijun Zhan; Ichiro Hasuo (FM (1), 2024)

CauMon: An Informative Online Monitor for Signal Temporal Logic. - Zhenya Zhang; Jie An 001; Paolo Arcaini; Ichiro Hasuo (FM (2), 2024)

Learning Deterministic Multi-Clock Timed Automata. - Yu Teng; Miaomiao Zhang 003; Jie An 001 (HSCC, 2024)

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications (Artifact). - Sota Sato 001; Jie An 001; Zhang Zhenya; Ichiro Hasuo (Zenodo, 2024)

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications (Artifact). - Sota Sato 001; Jie An 001; Zhang Zhenya; Ichiro Hasuo (Zenodo, 2024)

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications (Artifact). - Sota Sato 001; Jie An 001; Zhang Zhenya; Ichiro Hasuo (Zenodo, 2024)

CauMon: An Informative Online Monitor for Signal Temporal Logic. - Zhenya Zhang; Jie An 001; Paolo Arcaini; Ichiro Hasuo (Zenodo, 2024)

Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. - Yue Fang; Zhi Jin; Jie An 001; Hongshen Chen; Xiaohong Chen; Naijun Zhan (ACL (Findings), 2025)

Derivative-Agnostic Inference of Nonlinear Hybrid Systems. - Hengzhi Yu; Bohan Ma; Mingshuai Chen; Jie An 001; Bin Gu 006; Naijun Zhan; Jianwei Yin (CoRR, 2025)

Componentwise Automata Learning for System Integration (Extended Version). - Hiroya Fujinami; Masaki Waga; Jie An 001; Kohei Suenaga; Nayuta Yanagisawa; Hiroki Iseri; Ichiro Hasuo (CoRR, 2025)