Publications

2023

Journal Articles

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}
}

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

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

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}
}

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}
}

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

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}
}

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

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

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

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}
}

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}
}

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}
}

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}
}

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

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}
}

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}
}

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}
}