Jie An (安杰), Ph.D., Associate Professor (Tenured), Ph.D. Advisor

Affiliation: Institute of Software, Chinese Academy of Sciences (ISCAS)

Address: 4# South Fourth Street, Zhong Guan Cun, Haidian District, Beijing, China

Postal Code: 100190

Email: anjie[@]iscas[DOT]ac[DOT]cn

Webpage: https://leslieaj.github.io/

We are constantly looking for self-motivated Postdocs, Ph.D./Master Students, and Research Assistants/Interns to join our group at ISCAS. The excellent postdocs can be appointed as the Special Research Associates of the Chinese Academy of Sciences. If you are interested in our work and would like to join us, please do not hesitate to send me an email with or without your CV to start a conversation!

Research Areas

My research interests lie in formal methods, with a focus on applying formal methods and machine learning to intelligent Cyber-Physical Systems (CPS) that underpin our daily lives to ensure their functionality, robustness, reliability, safety, security, etc.

Formal methods offer a mathematically interpretive and rigorous approach to modeling, analyzing, monitoring, and verifying CPS. However, the high complexity and undecidability can pose significant challenges in solving complicated problems effectively and efficiently. On the other hand, artificial intelligence techniques has demonstrated effectiveness in various practical applications, but often lacks interpretability and guarantees. Consequently, finding ways to combine lightweight formal methods and interpretable artificial intelligence techniques to address CPS-related problems presents an exciting research area, but one that requires balancing the trade-off between exactness and effectiveness.

My current research topics include but are not limited to

- Formal Methods + Artificial Intelligence
- Model Learning & System Identification
- Modeling, Monitoring, Falsification, Verification, Synthesis of Real-time Systems, Embedded Systems, and CPS
- CPS Privacy and Security


Education

  • 2015~2020, Tongji University, Shanghai, China, Ph.D. of Software Engineering 

  • 2012~2015, Tongji University, Shanghai, China, Master of Software Engineering 

  • 2008~2012, Tongji University, Shanghai, China, Bachelor of Software Engineering



Experience


Publications

  • Yue Fang, Zhi Jin, Jie An, Jia Li, Hongshen Chen, Xiaohong Chen, Naijun Zhan. ClarifySTL: An Interactive Agent Framework for STL Transformation through Requirements Clarification. ACM Transactions on Software Engineering and Methodology (ACM TOSEM).
  • Ziran Wang, Jie An, Naijun Zhan. Mining Deterministic Timed Automata with SMT by Exploiting Simple Elementary Language and Timed Augmented Prefix Acceptor. In Proceedings of the 47th IEEE Real-Time Systems Symposium (RTSS 2026).
  • Jiyu Zhu, Shenghua Feng, Jie An, Naijun Zhan. PAC Verification of STL for Linear Parabolic PDEs. In Proceedings of the 2026 ACM/IEEE International Conference on Embedded Software (EMSOFT 2026).
  • Shenhua Feng, Hao Wu, Han Su, Jie An, Mingshuai Chen and Naijun Zhan. Tolerant Barrier Certificates for Stochastic Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD). (A special issue of EMSOFT 2026).
  • Zhenya Zhang, Parv Kapoor, Jie An and Eunsuk Kang. Counterexample Classification for Signal Temporal Logic Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD). (A special issue of EMSOFT 2026).
  • Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan and Fanjiang Xu. How Powerful are LLMs in Generating Program Specifications? In Proceedings of the 43rd International Conference on Machine Learning (ICML 2026).
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Jiangmeng Li, Xiaohong Chen and Naijun Zhan. PRM-PBE: Process Reward Model for Reinforcement Learning in Programming-by-Example. In Proceedings of the 43rd International Conference on Machine Learning (ICML 2026).
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. CauMon: A Tool for Online Monitoring against Signal Temporal Logic. Science of Computer Programming (SCP), 253, 103499:1--103499:5.
  • Hongjing Qing, Jie An and Fanjiang Xu. LLM-Enhanced Two-Stage STL Generation with Structured Intermediate Representation. In Proceedings of the 63rd Design Automation Conference (DAC 2026).
  • Martin Jouve-Genty, Han Su, Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo. STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP. In Proceedings of the 27th International Symposium on Formal Methods (FM 2026).
  • Shenghua Feng, Jie An, Naijun Zhan and Fanjiang Xu. Exact Moment Estimation of Stochastic Differential Dynamics. In Proceedings of the 27th International Symposium on Formal Methods (FM 2026).
  • Hengzhi Yu, Bohan Ma, Mingshuai Chen, Huangying Dong, Jie An, Bin Gu, Naijun Zhan and Jianwei Yin. Derivative-Agnostic Inference of Nonlinear Hybrid Systems. In Proceedings of the 29th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2026).
  • Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan. Quantifier Elimination Meets Treewidth. In Proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS/ETAPS 2026).
  • Shenghua Feng, Jie An and Fanjiang Xu. Runtime Safety and Reach-Avoid Prediction of Stochastic Systems with Observation-Aware Barrier Functions. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen and Naijun Zhan. RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  • Juejie Meng, Jie An, Yong Li, Andrea Turrini and Miaomiao Zhang. SAT-based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation. In Proceedings of the 27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026).
  • Xiaochen Tang, Zhenya Zhang, Miaomiao Zhang and Jie An. Control Synthesis of Cyber-Physical Systems for Real-Time Specifications through Causation-Guided Reinforcement Learning. In Proceedings of the 46th IEEE Real-Time Systems Symposium (RTSS 2025).
  • Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang and Zhenya Zhang. On Synthesis of Timed Regular Expressions. In Proceedings of the 46th IEEE Real-Time Systems Symposium (RTSS 2025).
  • Hiroya Fujinami, Masaki Waga, Jie An, Kohei Suenaga, Nayuta Yanagisawa, Hiroki Iseri and Ichiro Hasuo. Componentwise Automata Learning for System Integration. In Proceedings of the 23rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2025), pp. 3--26.
  • Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan and Miaomiao Zhang. Efficient Decomposition Identification of Deterministic Finite Automata from Examples. In Proceedings of the 11th International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2025). To appear.
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen and Naijun Zhan. Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL 2025). pp. 10446--10458.
  • Chengzi Huang, Behnam Khodabandeloo, Duc Anh Nguyen, Wang Yi, Jie An and Zhenya Zhang. Causality Monitoring for MIMOS. Principles of Formal Quantitative Analysis -- Essays dedicated to Christel Baier on the occasion of her 60th birthday (PFQA-Baier60). pp. 284--300.
  • Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang, Jie An and Naijun Zhan. Active Learning of Deterministic Timed Automata via Timed Classification Tree. SCIENCE CHINA Information Sciences (SCIS), 68(12), 222101:1--222101:17.
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. CauMon: An Informative Online Monitor for Signal Temporal Logic. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Part II, pp. 286--304. 
  • Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan and Ichiro Hasuo. The Opacity of Timed Automata. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Part I, pp. 620--637.
  • Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo. Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications. In Proceedings of the 36th International Conference on Computer Aided Verification (CAV 2024), Part III, pp. 282--306. 
  • Yu Teng, Miaomiao Zhang and Jie An. Learning Deterministic Multi-Clock Timed Automata. In Proceedings of the 27th International Conference on Hybrid Systems: Control and Computation (HSCC 2024), pp. 6:1--6:11.
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. Online Causation Monitoring of Signal Temporal Logic. In Proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023), Part I, pp. 62--84. 
  • Runqing Xu, Jie An and Bohua Zhan. Active learning of One-Clock Timed Automata using Constraint Solving. In Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pp. 249--265.
  • Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan and Naijun Zhan. Learning Deterministic One-Clock Timed Automata via Mutation Testing. In Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pp. 233--248.
  • Junri Mi, Miaomiao Zhang, Jie An and Bowen Du. Learning Deterministic One-Clock Timed Automata Based on Timed Classification Tree. Journal of Software, 33(8), 2797--2814. (in Chinese)
  • Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning Nondeterministic Real-Time Automata. ACM Transactions on Embedded Computing Systems (ACM TECS), 20(5s), 99:1--99:26. (Special issue of EMSOFT/ESWEEK 2021) 
  • Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Inferring Switched Nonlinear Dynamical Systems. Formal Aspects of Computing (FAC), 33(3), 385--406.
  • Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning Real-Time Automata. SCIENCE CHINA Information Sciences (SCIS), 64(9), 192103:1--192103:17.
  • Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue and Naijun Zhan. PAC Learning of Deterministic One-Clock Timed Automata. In Proceedings of the 22nd International Conference on Formal Engineering Methods (ICFEM 2020), pp. 129--146.
  • Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning One-Clock Timed Automata. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS/ETAPS 2020), pp. 444--462. 
  • Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang and Ting Gan. From Model to Implementation: A Network-Algorithm Programming Language. SCIENCE CHINA Information Sciences (SCIS), 63(7), 172102:1--172102:17.
  • Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur and Naijun Zhan. NIL: Learning Nonlinear Interpolants. In Proceedings of the 27th International Conference on Automated Deduction (CADE-27), pp. 178--196.
  • Xiaoxue Hou, Jie An, Miaomiao Zhang, Bowen Du and Jing Liu. High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training. In Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2019), pp. 840--847.
  • Jie An, Miaomiao Zhang. Verifying Continuous-Time Duration Calculus Against Real-Time Automaton. Journal of Software, 30(7), 1953--1965. (in Chinese)
  • Lingtai Wang, Naijun Zhan and Jie An. The Opacity of Real-time Automata. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 37(11), 2845--2856. (Special issue of EMSOFT/ESWEEK 2018)
  • Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang and Wang Yi. Model Checking Bounded Continuous-Time Extended Linear Duration Invariants. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (HSCC 2018), pp. 81--90. (part of CPS Week 2018)

Academy Services


Students


Ph.D. Students
Hongjing Qing (2025) Yihao Yin (2026) Chenchen Hong (2026)
Master Students
Yilin An (2026)
Visiting Students / Interns
Yue Fang (Ph.D student from Peking University)

Honors & Distinctions

  • Distinguished Paper Award at ATVA 2025, October 2025
  • Springer Nature High-Impact Publications in Computer Science, August 2020
  • Best Paper Award at FMAC 2019, December 2019