基本信息
李勇  男  硕导  中国科学院软件研究所
电子邮件： 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） 中科院百篇优秀博士论文, 院级, 2022
专利成果
（ 1 ） Chisel断言语言的类SVA扩展及形式化验证方法, 发明专利, 2023, 第 3 作者, 专利号: CN 115496017 B

出版信息

   
发表论文
（1） On the Power of Finite Ambiguity in B\"uchi Complementation, Infomation and Computation, 2023, 第 2 作者
（2） Divide-and-Conquer Determinization of B��chi Automata Based on SCC Decomposition, CAV, 2022, 第 1 作者
（3） Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper), SEFM 2022, 2022, 第 4 作者
（4） 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 作者
（5） Büchi自动机学习与取补的新算法的研究, 2019, 第 1 作者

科研活动

   
科研项目
（ 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/）