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

Jie An's Homepage

photo 

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

  • 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).
    In press.

  • 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

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