基本信息
李勇 男 硕导 中国科学院软件研究所
电子邮件： liyong@ios.ac.cn
通信地址： 北京市海淀区中关村南四街4号5号楼218
邮政编码： 100190
电子邮件： liyong@ios.ac.cn
通信地址： 北京市海淀区中关村南四街4号5号楼218
邮政编码： 100190
研究领域
形式化方法，包括自动机理论与模型验证技术
招生信息
如果你是一名对以下方向感兴趣的高年级本科生，欢迎联系我（包括硕士研究生保送推荐与考试）。
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. ATVAnull. 2023, 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. ATVAnull. 2023, 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. CONCURnull. 2023, https://doi.org/10.4230/LIPIcs.CONCUR.2023.37.[4] Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y Vardi, Lijun Zhang. Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. CAVnull. 2023, 152-173, http://dx.doi.org/10.1007/978-3-031-13188-2_8.[5] 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, 180: http://dx.doi.org/10.1016/j.ipl.2022.106342.[6] 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 2015null. 2015, 9409: 35-51, [7] Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y Vardi, Lijun Zhang. On the power of finite ambiguity in Büchi complementation. INFORMATION AND COMPUTATION. http://dx.doi.org/10.1016/j.ic.2023.105032.[8] Yi Li, Xie Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang. Synthesizing ranking functions for loop programs via SVM. THEORETICAL COMPUTER SCIENCE. 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/）