Jie An's Homepage

I am a postdoctoral researcher at Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany. I work in the Rigorous Software Engineering Group headed by Prof.Dr. Rupak Majumdar. 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. (jiean[@]mpi-sws[DOT]org) Github

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

• 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

• Learning One-Clock Timed Automata. Presented at AMMS 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

• External reviewer

  • ADHS 2021, CAV 2021, HSCC 2021, TASE 2021.

  • iFM 2020, RTSS 2020, HSCC 2020, TASE 2020.

  • EMSOFT 2019, RTSS 2019, ICFEM 2019.

• Journal reviewer

  • TOSEM

• Organization committee member of SSFM 2018, SSFM 2019 (the Summer School on Formal Methods at the State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences).

• Volunteer of CONFESTA 2018.

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).