2023

Journal Articles

  1. Hu, M., Zhang, M., Mallet, F., Fu, X., and Chen, M. 2023. Accelerating Reinforcement Learning-Based CCSL Specification Synthesis Using Curiosity-Driven Exploration. IEEE Trans. Computers 72, 5, 1431–1446. DOI
    @article{HuZMFC23,
      author = {Hu, Ming and Zhang, Min and Mallet, Fr{\'{e}}d{\'{e}}ric and Fu, Xin and Chen, Mingsong},
      title = {Accelerating Reinforcement Learning-Based {CCSL} Specification Synthesis
                        Using Curiosity-Driven Exploration},
      journal = {{IEEE} Trans. Computers},
      volume = {72},
      number = {5},
      pages = {1431--1446},
      year = {2023},
      doi = {10.1109/TC.2022.3197956}
    }
    
  2. Hu, M., Xia, J., Zhang, M., Chen, X., Mallet, F., and Chen, M. 2023. Automated Synthesis of Safe Timing Behaviors for Requirements Models Using CCSL. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 42, 12, 5127–5140. DOI
    @article{HuXZCMC23,
      author = {Hu, Ming and Xia, Jun and Zhang, Min and Chen, Xiaohong and Mallet, Fr{\'{e}}d{\'{e}}ric and Chen, Mingsong},
      title = {Automated Synthesis of Safe Timing Behaviors for Requirements Models
                        Using {CCSL}},
      journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
      volume = {42},
      number = {12},
      pages = {5127--5140},
      year = {2023},
      doi = {10.1109/TCAD.2023.3285412}
    }
    

chapter

  1. Mallet, F. 2023. Time: It is only Logical! In: J.P. Bowen, Q. Li and Q. Xu, eds., Theories of Programming and Formal Methods. Springer, 323–347. DOI
    @chapter{Mallet23,
      author = {Mallet, Fr{\'{e}}d{\'{e}}ric},
      editor = {Bowen, Jonathan P. and Li, Qin and Xu, Qiwen},
      title = {Time: It is only Logical!},
      booktitle = {Theories of Programming and Formal Methods},
      series = {Lecture Notes in Computer Science},
      volume = {14080},
      pages = {323--347},
      publisher = {Springer},
      year = {2023},
      doi = {10.1007/978-3-031-40436-8\_12}
    }
    

2022

Journal Articles

  1. Zhang, Y., Mallet, F., and Liu, Z. 2022. A dynamic logic for verification of synchronous models based on theorem proving. Frontiers Comput. Sci. 16, 4, 164407. URL DOI
    @article{ZhangML22,
      author = {Zhang, Yuanrui and Mallet, Fr{\'{e}}d{\'{e}}ric and Liu, Zhiming},
      journal = {Frontiers Comput. Sci.},
      title = {A dynamic logic for verification of synchronous models based on theorem proving},
      year = {2022},
      number = {4},
      pages = {164407},
      volume = {16},
      doi = {10.1007/s11704-022-1374-4},
      timestamp = {Wed, 18 May 2022 18:07:44 +0200},
      url = {https://doi.org/10.1007/s11704-022-1374-4}
    }
    
  2. Chen, X., Liu, Q., Mallet, F., Li, Q., Cai, S., and Jin, Z. 2022. Formally verifying consistency of sequence diagrams for safety critical systems. Sci. Comput. Program. 216, 102777. URL DOI
    @article{ChenLMLCJ22,
      author = {Chen, Xiaohong and Liu, Qianqian and Mallet, Fr{\'{e}}d{\'{e}}ric and Li, Qin and Cai, Shubin and Jin, Zhi},
      journal = {Sci. Comput. Program.},
      title = {Formally verifying consistency of sequence diagrams for safety critical systems},
      year = {2022},
      pages = {102777},
      volume = {216},
      doi = {10.1016/j.scico.2022.102777},
      timestamp = {Fri, 01 Apr 2022 11:23:07 +0200},
      url = {https://doi.org/10.1016/j.scico.2022.102777}
    }
    
  3. Ameur-Boulifa, R., Henrio, L., and Madelaine, E. 2022. Compositional Equivalences Based on Open pNets. Journal of Logical and Algebraic Methods in Programming. URL
    @article{hal-03894031,
      author = {Ameur-Boulifa, Rab{\'e}a and Henrio, Ludovic and Madelaine, Eric},
      journal = {{Journal of Logical and Algebraic Methods in Programming}},
      title = {{Compositional Equivalences Based on Open pNets}},
      year = {2022},
      hal_id = {hal-03894031},
      hal_version = {v1},
      keywords = {Bisimulation ; compositionality ; automata ; semantics},
      pdf = {https://hal.archives-ouvertes.fr/hal-03894031/file/WeakBisim.pdf},
      publisher = {{Elsevier}},
      url = {https://hal.archives-ouvertes.fr/hal-03894031}
    }
    

2021

Journal Articles

  1. Zhang, Y., Mallet, F., Zhu, H., Chen, Y., Liu, B., and Liu, Z. 2021. A clock-based dynamic logic for schedulability analysis of CCSL specifications. Sci. Comput. Program. 202, 102546. DOI
    @article{Zhang2021,
      author = {Zhang, Yuanrui and Mallet, Fr{\'{e}}d{\'{e}}ric and Zhu, Huibiao and Chen, Yixiang and Liu, Bo and Liu, Zhiming},
      title = {A clock-based dynamic logic for schedulability analysis of {CCSL} specifications},
      journal = {Sci. Comput. Program.},
      year = {2021},
      volume = {202},
      pages = {102546},
      doi = {10.1016/j.scico.2020.102546}
    }
    
  2. Zhang, Y., Wu, H., Chen, Y., and Mallet, F. 2021. A clock-based dynamic logic for the verification of CCSL specifications in synchronous systems. Sci. Comput. Program. 203, 102591. URL DOI
    @article{Zhang2021a,
      author = {Zhang, Yuanrui and Wu, Hengyang and Chen, Yixiang and Mallet, Fr{\'{e}}d{\'{e}}ric},
      title = {A clock-based dynamic logic for the verification of {CCSL} specifications in synchronous systems},
      journal = {Sci. Comput. Program.},
      year = {2021},
      volume = {203},
      pages = {102591},
      doi = {10.1016/j.scico.2020.102591},
      url = {https://hal.inria.fr/hal-03135428}
    }
    

Conference Articles

  1. Hu, M., Ding, J., Zhang, M., Mallet, F., and Chen, M. 2021. Enumeration and Deduction Driven Co-Synthesis of CCSL Specifications Using Reinforcement Learning. 42nd IEEE Real Time Systems Symposium (RTSS 2021).
    @inproceedings{Hu2021,
      author = {Hu, Ming and Ding, Jiepin and Zhang, Min and Mallet, Fr\'ed\'eric and Chen, Mingsong},
      title = {Enumeration and Deduction Driven Co-Synthesis of CCSL Specifications Using Reinforcement Learning},
      booktitle = {42nd IEEE Real Time Systems Symposium (RTSS 2021)},
      year = {2021},
      month = dec
    }
    

Technical Reports

  1. Wang, B., Madelaine, E., and Zhang, M. 2021. Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version. Inria \& Université Cote d’Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai). URL
    @techreport{wang:hal-03126313,
      title = {{Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version}},
      author = {Wang, Biyang and Madelaine, Eric and Zhang, Min},
      url = {https://hal.inria.fr/hal-03126313},
      type = {Research Report},
      number = {RR-9389},
      pages = {71},
      institution = {{Inria \\& Universit{\'e} Cote d'Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai)}},
      year = {2021},
      month = jan
    }
    

2020

Conference Articles

  1. Gao, F., Mallet, F., Zhang, M., and Chen, M. 2020. Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint. 2020 Design, Automation & Test in Europe Conference & Exhibition, DATE 2020, IEEE, 376–381. URL DOI
    @inproceedings{Gao2020,
      author = {Gao, Fei and Mallet, Fr{\'{e}}d{\'{e}}ric and Zhang, Min and Chen, Mingsong},
      title = {Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint},
      booktitle = {2020 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2020},
      year = {2020},
      pages = {376--381},
      month = mar,
      publisher = {{IEEE}},
      biburl = {https://dblp.org/rec/conf/date/GaoMZC20.bib},
      doi = {10.23919/DATE48585.2020.9116344},
      location = {Grenoble, France},
      timestamp = {Sun, 28 Jun 2020 19:41:15 +0200},
      url = {https://hal.archives-ouvertes.fr/hal-02429533}
    }
    
  2. Chen, X., Mallet, F., and Liu, X. 2020. Formally Verifying Sequence Diagrams for Safety Critical Systems. International Symposium on Theoretical Aspects of Software Engineering, TASE 2020, IEEE, 217–224. URL DOI
    @inproceedings{Chen2020,
      author = {Chen, Xiaohong and Mallet, Fr{\'{e}}d{\'{e}}ric and Liu, Xiaoshan},
      title = {Formally Verifying Sequence Diagrams for Safety Critical Systems},
      booktitle = {International Symposium on Theoretical Aspects of Software Engineering, {TASE} 2020},
      year = {2020},
      editor = {Aoki, Toshiaki and Li, Qin},
      pages = {217--224},
      month = dec,
      publisher = {{IEEE}},
      biburl = {https://dblp.org/rec/conf/tase/0007ML20.bib},
      doi = {10.1109/TASE49443.2020.00037},
      location = {Hangzhou, China},
      timestamp = {Tue, 27 Apr 2021 14:43:46 +0200},
      url = {https://doi.org/10.1109/TASE49443.2020.00037}
    }
    
  3. Hou, Z. and Madelaine, E. 2020. Symbolic bisimulation for open and parameterized systems. Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2020, ACM, 14–26. URL DOI
    @inproceedings{Hou2020,
      author = {Hou, Zechen and Madelaine, Eric},
      title = {Symbolic bisimulation for open and parameterized systems},
      booktitle = {Proceedings of the 2020 {ACM} {SIGPLAN} Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2020},
      year = {2020},
      editor = {Poulsen, Casper Bach and Hu, Zhenjiang},
      pages = {14--26},
      month = jan,
      publisher = {{ACM}},
      doi = {10.1145/3372884.3373161},
      location = {New Orleans, LA, USA},
      url = {https://doi.org/10.1145/3372884.3373161}
    }
    
  4. Liu, Q., Simone, R. de, Chen, X., et al. 2020. Multiform Logical Time & Space for Mobile Cyber-Physical System With Automated Driving Assistance System. 27th Asia-Pacific Software Engineering Conference, APSEC, IEEE, 415–424. URL DOI
    @inproceedings{Liu2020,
      author = {Liu, Qian and de Simone, Robert and Chen, Xiaohong and Kang, Jiexiang and Liu, Jing and Yin, Wei and Wang, Hui},
      title = {Multiform Logical Time {\&} Space for Mobile Cyber-Physical System With Automated Driving Assistance System},
      booktitle = {27th Asia-Pacific Software Engineering Conference, {APSEC}},
      year = {2020},
      pages = {415--424},
      month = dec,
      publisher = {{IEEE}},
      doi = {10.1109/APSEC51365.2020.00050},
      location = {Singapore},
      url = {https://doi.org/10.1109/APSEC51365.2020.00050}
    }
    
  5. Liu, Q., Simone, R. de, Chen, X., and Liu, J. 2020. Multiform Logical Time & Space for Specification of Automated Driving Assistance Systems: Work-in-Progress. 20th International Conference on Embedded Software, EMSOFT, IEEE, 22–24. URL DOI
    @inproceedings{Liu2020a,
      author = {Liu, Qian and de Simone, Robert and Chen, Xiaohong and Liu, Jing},
      title = {Multiform Logical Time {\&} Space for Specification of Automated Driving Assistance Systems: Work-in-Progress},
      booktitle = {20th International Conference on Embedded Software, {EMSOFT}},
      year = {2020},
      editor = {Mitra, Tulika and Gerstlauer, Andreas},
      pages = {22--24},
      month = sep,
      publisher = {{IEEE}},
      doi = {10.1109/EMSOFT51651.2020.9244041},
      location = {Singapore},
      url = {https://doi.org/10.1109/EMSOFT51651.2020.9244041}
    }
    

Journal Articles

  1. Mallet, F. and Zhang, M. 2020. Editorial - Theoretical Aspects of Software Engineering (2017). Sci. Comput. Program. 198, 102521. DOI
    @article{Mallet2020,
      author = {Mallet, Fr{\'{e}}d{\'{e}}ric and Zhang, Min},
      title = {Editorial - Theoretical Aspects of Software Engineering {(2017)}},
      journal = {Sci. Comput. Program.},
      year = {2020},
      volume = {198},
      pages = {102521},
      biburl = {https://dblp.org/rec/journals/scp/Mallet020.bib},
      doi = {10.1016/j.scico.2020.102521},
      timestamp = {Tue, 17 Nov 2020 16:14:56 +0100}
    }
    
  2. Zhang, Y., Mallet, F., and Chen, Y. 2020. A verification framework for spatio-temporal consistency language with CCSL as a specification language. Frontiers Comput. Sci. 14, 1, 105–129. DOI
    @article{Zhang2020,
      author = {Zhang, Yuanrui and Mallet, Fr{\'{e}}d{\'{e}}ric and Chen, Yixiang},
      title = {A verification framework for spatio-temporal consistency language with {CCSL} as a specification language},
      journal = {Frontiers Comput. Sci.},
      year = {2020},
      volume = {14},
      number = {1},
      pages = {105--129},
      biburl = {https://dblp.org/rec/journals/fcsc/ZhangMC20.bib},
      doi = {10.1007/s11704-018-7054-8},
      timestamp = {Fri, 09 Apr 2021 18:29:47 +0200}
    }
    
  3. Qin, X., Bliudze, S., Madelaine, E., Hou, Z., Deng, Y., and Zhang, M. 2020. SMT-based generation of symbolic automata. Acta Informatica 57, 3-5, 627–656. URL DOI
    @article{Qin2020,
      author = {Qin, Xudong and Bliudze, Simon and Madelaine, Eric and Hou, Zechen and Deng, Yuxin and Zhang, Min},
      title = {SMT-based generation of symbolic automata},
      journal = {Acta Informatica},
      year = {2020},
      volume = {57},
      number = {3-5},
      pages = {627--656},
      doi = {10.1007/s00236-020-00367-6},
      url = {https://doi.org/10.1007/s00236-020-00367-6}
    }