Jie An
Home
Reaserch interests
Publications
Tools
Useful links
jemdoc
Decision Procedures

Jie An's Homepage

photo 

I am an Associate Research Professor at the Institute of Software, Chinese Academy of Sciences (ISCAS), Beijing, China.

From October 2022 to May 2024, I was a Project Researcher and later a Project Assistant Professor at National Institute of Informatics (NII) in Tokyo, Japan, working in the project ERATO MMSD headed by Prof.Dr. Ichiro Hasuo. From November 2020 to October 2022, I was a Postdoctoral Researcher working in the Rigorous Software Engineering Group headed by Prof.Dr. Rupak Majumdar at Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany. I obtained my PhD degree in Software Engineering from School of Software Engineering, Tongji University in July 2020. (advisors: Miaomiao Zhang and Naijun Zhan). Before that, I also obtained my Bachelor degree and Master degree both in Software Engineering from the same university. From 2017 to 2020, I was also a visiting PhD student at SKLCS, Institute of Software, Chinese Academy of Sciences where I was advised by Prof.Dr. Naijun Zhan.

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

Github    DBLP    Google Scholar    ORCID

Research Interests

My current research interests include

  • Formal Methods + Machine Learning

  • Model Learning & System Identification

  • Modeling · Verification · Synthesis of real-time and embedded systems and cyber-physical systems

  • Programming Languages

Publications

  • Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo (2024).
    CauMon: An Informative Online Monitor for Signal Temporal Logic.
    In: International Symposium on Formal Methods (FM 2024).
    [Accepted]

  • Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo (2024).
    The Opacity of Timed Automata.
    In: International Symposium on Formal Methods (FM 2024).
    [Accepted]

  • Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo (2024).
    Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications.
    In: International Conference on Computer Aided Verification (CAV 2024), part III, pages 282-306.
    [Paper] (Artifact Evaluated)

  • Yu Teng, Miaomiao Zhang, Jie An (2024).
    Learning Deterministic Multi-Clock Timed Automata.
    In: International Conference on Hybrid Systems: Computation and Control (HSCC 2024), pages 6:1-6:11.
    [Paper] [Full version on arXiv]

  • Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo (2023).
    Online Causation Monitoring of Signal Temporal Logic.
    In: International Conference on Computer Aided Verification (CAV 2023), part I, pages 62-84.
    [Paper] [Full version on arXiv] (Artifact Evaluated)

  • Runqing Xu, Jie An, Bohua Zhan (2022).
    Active learning of One-Clock Timed Automata using Constraint Solving.
    In: International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pages 249-265.
    [Paper] [Full version on arXiv]

  • Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan (2022).
    Learning Deterministic One-Clock Timed Automata via Mutation Testing.
    In: International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pages 233-248.
    [Paper]

  • Junri Mi, Miaomiao Zhang, Jie An, Bowen Du (2022).
    Learning Deterministic One-clock Timed Automata Based on Timed Classification Tree.
    Journal of Software, 33(8): 2797-2814.

  • Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2021).
    Learning Nondeterministic Real-Time Automata.
    ACM Transactions on Embedded Computing Systems (ACM TECS), 20(5s): 99:1-99:26. (A special issue of EMSOFT 2021)
    [Paper]

  • Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2021).
    Inferring Switched Nonlinear Dynamical Systems.
    Formal Aspects of Computing (FAC). 33(3):385-406.
    [Paper]

  • Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan (2020).
    PAC Learning of Deterministic One-Clock Timed Automata.
    In: International Conference on Formal Engineering Methods (ICFEM 2020), pages 129-146.
    [Paper]

  • Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2020).
    Learning One-Clock Timed Automata.
    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), pages 444-462.
    [Paper] [Full version on arXiv] (Artifact Evaluated)

  • Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2020).
    Learning Real-Time Automata.
    SCIENCE CHINA Information Sciences (SCIS), 64(9): 192103:1-192103:17.
    [Paper]

  • Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan (2020).
    From model to implementation: A network-algorithm programming language.
    SCIENCE CHINA Information Sciences (SCIS), 63(7): 172102:1-172102:17.
    [Paper]

  • Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan (2019).
    NIL: Learning Nonlinear Interpolants.
    In: International Conference on Automated Deduction (CADE 27), pages 178-196.
    [Paper] [Full version on arXiv]

  • Xiaoxue Hou, Jie An, Miaomiao Zhang, Bowen Du, Jing Liu (2019).
    High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training.
    In: ICTAI 2019, pages 840-847.
    [Paper]

  • Jie An, Miaomiao Zhang (2019).
    Verifying Continuous-time Duration Calculus against Real-time Automaton.
    Journal of Software, 30(7): 1953-1965.

  • Lingtai Wang, Naijun Zhan, Jie An (2018).
    The Opacity of Real-Time Automata.
    IEEE Transactions on CAD of Integrated Circuits and Systems (IEEE TCAD), 37(11):2845-2856. (A special issue of EMSOFT 2018)
    [Paper]

  • Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi (2018).
    Model Checking Bounded Continuous-time Extended Linear Duration Invariants.
    In: International Conference on Hybrid Systems: Computation and Control (HSCC 2018), pages 81-90.
    [Paper]

Tools

  • NIL: A learning-based tool in Mathematica that is dedicated to synthesizing nontrivial (reverse) Craig interpolants for the quantifier-free theory of nonlinear arithmetic.

  • OTALearning: This prototype tool is dedicated to actively learning deterministic one-clock timed automata (DOTAs). (The evaluated artifact by TACAS-2020 is also archived in the Figshare repository.)

  • RTALearning: This prototype tool is dedicated to actively learning real-time automata (RTAs). A real-time automaton can be viewed as a timed automaton with only one clock which resets at every transition.

  • RTAOpacity: A prototype tool for deciding the language-opacity of real-time automata (RTAs).

  • VCELDI: A prototype tool to verify continuous-time Extend Linear Duration Inviriants (ELDIs) formulas againt timed automata (TAs).

  • NAPL: A declarative network algorithm programming language.

Presentations

  • Active Learning of One-Clock Timed Automata. Presented at CyPhAI Workshop 2022.

  • Learning Nondeterministic Real-Time Automata. Presented at EMSOFT 2021.

  • Learning One-Clock Timed Automata. Presented at TACAS 2021 (for the accepted paper in TACAS 2020).

  • Active Learning of Timed Systems. Presented at Academy of Mathematics and Systems Science, Chinese Academic of Sciences (AMSS CAS). 2019.

  • Learning One-Clock Timed Automata. Presented at FMAC 2019. (Best Paper Award)

  • The Opacity of Real-time Automata. Presented at YR-FMAC 2018.

  • Verifying Continuous-time Duration Calculus against Real-time Automata. Presented at FMAC 2018.

  • Model Checking Bounded Continuous-time Extended Linear Duration Invariants. Presented at the 21st ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2018).

  • Model Checking of Extended Linear Duration Invariants. Presented at the Colloquium on Logic in Engineering Dependable Software (LEDS 2017).

Academic Services & TA

Academic Services

TA

  • Formal methods in software engineering. Autumn 2015 (for M.S. students).

  • Formal methods in software engineering. Autumn 2014 (for M.S. students).

  • Real-time Systems. Spring 2013 (for undergraduates).