李勇-中国科学院大学-UCAS

研究领域

形式化方法，包括自动机理论与模型验证技术

招生信息

如果你是一名对以下方向感兴趣的高年级本科生，欢迎联系我（包括硕士研究生保送推荐与考试）。
1、计算逻辑（比如时序逻辑、字符串约束等）,

2、形式语言与自动机理论（比如正规表达式、有限自动机、Omega自动机等）

3、基于SAT/SMT的模型验证技术。

更多信息请访问个人主页：https://liyong31.github.io/

招生专业

081202-计算机软件与理论

招生方向

模型验证，自动机理论

教育背景

2013-08--2020-01 中国科学院大学、中国科学院软件研究所工学博士
2009-09--2013-06 南京邮电大学工学学士

学位

工学博士（专业：计算机软件与理论）

工作经历

2022-10~至今,中国科学院软件研究所、计算机科学国家重点实验室, 副研究员

2022-10~2024-10,英国利物浦大学、计算机科学系、Marie Curie Research Fellow

2020-04~2022-10,中科院软件所、计算机科学国家重点实验室、特别研究助理

专利与奖励

（1） Marie Curie Research Fellowship, 2022-10~2024-10

（2）中科院百篇优秀博士论文， 2022

专利成果

（ 1 ） Chisel断言语言的类SVA扩展及形式化验证方法, 发明专利, 2023, 第 3 作者, 专利号: CN 115496017 B

出版信息

发表论文

[1] Suguman Bansal, 李勇, Lucas M. Tabajara, Moshe Y. Vardi, Andrew Wells. Model Checking Strategies from Synthesis over Finite Traces. ATVA. 2023, 第 11 作者https://doi.org/10.1007/978-3-031-45329-8\_11.
[2] 李勇, Sven Schewe, Qiyi Tang. A Novel Family of Finite Automata for Recognizing and Learning omega-Regular Languages. ATVA. 2023, 第 1 作者https://doi.org/10.1007/978-3-031-45329-8\_3.
[3] 李勇, Sven Schewe, Moshe Y. Vardi. Singly Exponential Translation of Alternating Weak B��chi Automata to Unambiguous B��chi Automata. CONCUR. 2023, 第 1 作者https://doi.org/10.4230/LIPIcs.CONCUR.2023.37.
[4] Fu, Jianling, Huang, ChengChao, Li, Yong, Mei, Jingyi, Xu, Ming, Zhang, Lijun. Quantitative controller synthesis for consumption Markov decision processes. INFORMATION PROCESSING LETTERS[J]. 2023, 第 3 作者180: http://dx.doi.org/10.1016/j.ipl.2022.106342.
[5] Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y Vardi, Lijun Zhang. On the power of finite ambiguity in B��chi complementation. INFORMATION AND COMPUTATION[J]. 2023, 第 11 作者http://dx.doi.org/10.1016/j.ic.2023.105032.
[6] Weizhi Feng, Yong Li, Andrea Turrini, Moshe Vardi, Lijun Zhang. On the Power of Finite Ambiguity in B\"uchi Complementation. Infomation and Computation[J]. 2023, 第 2 作者292(105032):
[7] Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y Vardi, Lijun Zhang. Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. CAV. 2022, 第 1 作者152-173, http://dx.doi.org/10.1007/978-3-031-13188-2_8.
[8] 于世禛, 董一凡, 刘玖阳, 李勇, 吴志林, David N. Jansen, 张立军. Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). SEFM 2022. 2022, 第 4 作者
[9] 李勇, Andrea Turrini, 冯维直, Moshe Vardi, 张立军. Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. 2022, 第 1 作者
[10] 李勇. Büchi自动机学习与取补的新算法的研究. 2019, 第 1 作者
[11] van Dijk Tom, Hahn Ernst Moritz, Jansen David N, Li Yong, Neele Thomas, Stoelinga Marielle, Turrini Andrea, Zhang Lijun, Li X, Liu Z, Yi W. A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015. 2015, 第 4 作者9409: 35-51,
[12] Yi Li, Xie Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang. Synthesizing ranking functions for loop programs via SVM. THEORETICAL COMPUTER SCIENCE. 第 11 作者http://dx.doi.org/10.1016/j.tcs.2022.07.002.

科研活动

科研项目

（ 1 ） Büchi自动机的若干基础问题研究, 负责人, 国家任务, 2022-01--2024-12

合作情况

与国内外同行有广泛合作。国外合作包括：
-- 美国：Rice University的Moshe Vardi教授(https://www.cs.rice.edu/~vardi/)

-- 英国：University of Liverpool的Sven Schewe教授(https://intranet.csc.liv.ac.uk/~sven/)

-- 捷克：Brno University of Technology的Ondrej Lengal博士（https://www.fit.vutbr.cz/~lengal/）

-- 台湾：中央研究院资讯研究所的陈郁方博士（https://www.iis.sinica.edu.tw/pages/yfc/）