基本信息
吕毅 男 硕导 中国科学院软件研究所
电子邮件： lvyi@ios.ac.cn
通信地址： 中科院软件所计算机科学国家重点实验室
邮政编码： 100190
电子邮件： lvyi@ios.ac.cn
通信地址： 中科院软件所计算机科学国家重点实验室
邮政编码： 100190
招生信息
招生专业
081202-计算机软件与理论
085400-电子信息
085400-电子信息
招生方向
网络与并发实时系统的设计与分析
形式验证
模型检测
形式验证
模型检测
教育背景
2000-09--2004-07 中国科学院计算技术研究所 获博士学位
1997-09--2000-07 中国科学院计算技术研究所 获硕士学位
1989-09--1993-07 电子科技大学 获学士学位
1997-09--2000-07 中国科学院计算技术研究所 获硕士学位
1989-09--1993-07 电子科技大学 获学士学位
工作经历
工作简历
2009-01~现在, 中国科学院软件研究所, 副研究员
2007-02~2008-12,中国科学院软件研究所, 助理研究员
2004-08~2007-01,中国科学院软件研究所, 博士后
1993-08~1997-08,南京电子技术研究所, 助理工程师
2007-02~2008-12,中国科学院软件研究所, 助理研究员
2004-08~2007-01,中国科学院软件研究所, 博士后
1993-08~1997-08,南京电子技术研究所, 助理工程师
教授课程
并发数据结构与多核编程
多处理器系统编程
多处理器系统编程
出版信息
发表论文
[1] Qiaowen Jia, Yi Lv, Peng Wu, Bohua Zhan, Jifeng Hao, Hong Ye, Chao Wang. VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. TASE 2023. 2023, 第 2 作者
[2] 王超, 吕毅, 吴鹏, 贾巧雯. TSO 内存模型下限界可线性化的可判定性研究. 软件学报[J]. 2022, 第 2 作者 通讯作者 33(8): 2896-2917,
[3] Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. ITP 2022. 2022, 第 2 作者
[4] Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu. Decidability of Liveness for Concurrent Objects on the TSO Memory Model. 8th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2022). 2022, 第 3 作者
[5] Wang, Chao, Lv, Yi, Wu, Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2018, 第 2 作者61(1): https://www.webofscience.com/wos/woscc/full-record/WOS:000409915100006.
[6] Li, Yongjian, Duan, Kaiqiang, Jansen, David N, Pang, Jun, Zhang, Lijun, Lv, Yi, Cai, Shaowei. An Automatic Proving Approach to Parameterized Verification. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC[J]. 2018, 第 6 作者19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.
[7] Wang, Chao, Lv, Yi, Wu, Peng. TSO-to-TSO linearizability is undecidable. ACTA INFORMATICA[J]. 2018, 第 2 作者 通讯作者 55(8): 649-668, http://dx.doi.org/10.1007/s00236-017-0305-6.
[8] Wang, Chao, Lv, Yi, Wu, Peng, Steffen, B, Baier, C, VanDenBrand, M, Eder, J, Hinchey, M, Margaria, T. Decomposable Relaxation for Concurrent Data Structures. SOFSEM 2017: THEORY AND PRACTICE OF COMPUTER SCIENCE. 2017, 第 2 作者10139: 188-202,
[9] Wang Chao, Lv Yi, Wu Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2017, 第 2 作者61(1):
[10] Li, Yongjian, Duan, Kaiqiang, Lv, Yi, Pang, Jun, Cai, Shaowei, IEEE. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. PROCEEDINGS OF THE 34TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD). 2016, 第 3 作者560-567,
[11] 吕毅. Bounded TSO-to-SC Linearizability is Decidable. SOFSEM2016. 2016, 第 1 作者
[12] Ji Wei, Wang Farn, Wu Peng, Lv Yi, Wang H, Mokhtari M. An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata. 2016 21ST INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2016). 2016, 第 4 作者111-121, http://dx.doi.org/10.1109/ICECCS.2016.12.
[13] 吕毅. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols. ATVA2015. 2015, 第 1 作者
[14] Wang Chao, Lv Yi, Liu Gaoang, Wu Peng, Feng X, Park S. Quasi-Linearizability is Undecidable. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015. 2015, 第 2 作者9458: 369-386,
[15] Yue, Han, Wu, Peng, Chen, TsongYueh, Lv, Yi, Sun, J, Reddy, YR, Bahulkar, A, Pasala, A. Input-driven Active Testing of Multi-threaded Programs. 2015 22ND ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2015). 2015, 第 4 作者246-253,
[16] Wang Chao, Lv Yi, Wu Peng, Finkbeiner B, Pu G, Zhang L. TSO-to-TSO Linearizability Is Undecidable. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015. 2015, 第 2 作者9364: 309-325,
[17] Lv, Yi, Sun, Luming, Ye, Xiaochun, Fan, Dongrui, Wu, Peng, Cassez, F, Raskin, JF. Efficiently and Completely Verifying Synchronized Consistency Models. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014. 2014, 第 1 作者 通讯作者 8837: 264-280,
[18] Zheng Lv, Chen Hao, Chen Feng, Yi Lv. Fast verification of memory consistency for chip multi-processor. PROCEEDINGS - 2011 7TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND SECURITY, CIS 2011. 2011, 第 4 作者1497-1502, http://ir.iscas.ac.cn/handle/311060/16296.
[19] Guo Yan, Wang Yu, Ding Guodong, Cao Donglin, Zhang Gang, Lv Yi, Chen H, Yang CC, Chau M, Li SH. Juicer: Scalable Extraction for Thread Meta-information of Web Forum. INTELLIGENCE AND SECURITY INFORMATICS, PROCEEDINGS. 2009, 第 6 作者5477: 143-+,
[20] Pan Hong, 吕毅, 林惠民. Environment abstraction with state clustering and parameter truncating. PROCEEDINGS - 2009 3RD IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2009. 2009, 第 2 作者http://124.16.136.157/handle/311060/8304.
[21] Chen Yunji, Lv Yi, Hu Weiwu, Chen Tianshi, Shen Haihua, Wang Pengyu, Pan Hong, IEEE Comp Soc. Fast Complete Memory Consistency Verification. HPCA-15 2009: FIFTEENTH INTERNATIONAL SYMPOSIUM ON HIGH-PERFORMANCE COMPUTER ARCHITECTURE, PROCEEDINGS. 2009, 第 2 作者381-+,
[22] Lv Yi, Lin Huimin, Pan Hong. Computing invariants for parameter abstraction. PROCEEDINGS - FIFTH ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, MEMOCODE07. 2007, 第 1 作者29-38, http://124.16.136.157/handle/311060/10950.
[23] 吕毅, 王源, 李晓林. 服务网格的用户3A使用模式. 电子学报[J]. 2007, 第 1 作者35(2): 292-298, http://lib.cqvip.com/Qikan/Article/Detail?id=23918923.
[24] Pan, Hong, Lin, HuiMin, Lv, Yi. Model checking data consistency for cache coherence protocols. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2006, 第 3 作者21(5): 765-775, https://www.webofscience.com/wos/woscc/full-record/WOS:000240962200014.
[2] 王超, 吕毅, 吴鹏, 贾巧雯. TSO 内存模型下限界可线性化的可判定性研究. 软件学报[J]. 2022, 第 2 作者 通讯作者 33(8): 2896-2917,
[3] Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. ITP 2022. 2022, 第 2 作者
[4] Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu. Decidability of Liveness for Concurrent Objects on the TSO Memory Model. 8th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2022). 2022, 第 3 作者
[5] Wang, Chao, Lv, Yi, Wu, Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2018, 第 2 作者61(1): https://www.webofscience.com/wos/woscc/full-record/WOS:000409915100006.
[6] Li, Yongjian, Duan, Kaiqiang, Jansen, David N, Pang, Jun, Zhang, Lijun, Lv, Yi, Cai, Shaowei. An Automatic Proving Approach to Parameterized Verification. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC[J]. 2018, 第 6 作者19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.
[7] Wang, Chao, Lv, Yi, Wu, Peng. TSO-to-TSO linearizability is undecidable. ACTA INFORMATICA[J]. 2018, 第 2 作者 通讯作者 55(8): 649-668, http://dx.doi.org/10.1007/s00236-017-0305-6.
[8] Wang, Chao, Lv, Yi, Wu, Peng, Steffen, B, Baier, C, VanDenBrand, M, Eder, J, Hinchey, M, Margaria, T. Decomposable Relaxation for Concurrent Data Structures. SOFSEM 2017: THEORY AND PRACTICE OF COMPUTER SCIENCE. 2017, 第 2 作者10139: 188-202,
[9] Wang Chao, Lv Yi, Wu Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2017, 第 2 作者61(1):
[10] Li, Yongjian, Duan, Kaiqiang, Lv, Yi, Pang, Jun, Cai, Shaowei, IEEE. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. PROCEEDINGS OF THE 34TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD). 2016, 第 3 作者560-567,
[11] 吕毅. Bounded TSO-to-SC Linearizability is Decidable. SOFSEM2016. 2016, 第 1 作者
[12] Ji Wei, Wang Farn, Wu Peng, Lv Yi, Wang H, Mokhtari M. An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata. 2016 21ST INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2016). 2016, 第 4 作者111-121, http://dx.doi.org/10.1109/ICECCS.2016.12.
[13] 吕毅. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols. ATVA2015. 2015, 第 1 作者
[14] Wang Chao, Lv Yi, Liu Gaoang, Wu Peng, Feng X, Park S. Quasi-Linearizability is Undecidable. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015. 2015, 第 2 作者9458: 369-386,
[15] Yue, Han, Wu, Peng, Chen, TsongYueh, Lv, Yi, Sun, J, Reddy, YR, Bahulkar, A, Pasala, A. Input-driven Active Testing of Multi-threaded Programs. 2015 22ND ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2015). 2015, 第 4 作者246-253,
[16] Wang Chao, Lv Yi, Wu Peng, Finkbeiner B, Pu G, Zhang L. TSO-to-TSO Linearizability Is Undecidable. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015. 2015, 第 2 作者9364: 309-325,
[17] Lv, Yi, Sun, Luming, Ye, Xiaochun, Fan, Dongrui, Wu, Peng, Cassez, F, Raskin, JF. Efficiently and Completely Verifying Synchronized Consistency Models. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014. 2014, 第 1 作者 通讯作者 8837: 264-280,
[18] Zheng Lv, Chen Hao, Chen Feng, Yi Lv. Fast verification of memory consistency for chip multi-processor. PROCEEDINGS - 2011 7TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND SECURITY, CIS 2011. 2011, 第 4 作者1497-1502, http://ir.iscas.ac.cn/handle/311060/16296.
[19] Guo Yan, Wang Yu, Ding Guodong, Cao Donglin, Zhang Gang, Lv Yi, Chen H, Yang CC, Chau M, Li SH. Juicer: Scalable Extraction for Thread Meta-information of Web Forum. INTELLIGENCE AND SECURITY INFORMATICS, PROCEEDINGS. 2009, 第 6 作者5477: 143-+,
[20] Pan Hong, 吕毅, 林惠民. Environment abstraction with state clustering and parameter truncating. PROCEEDINGS - 2009 3RD IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2009. 2009, 第 2 作者http://124.16.136.157/handle/311060/8304.
[21] Chen Yunji, Lv Yi, Hu Weiwu, Chen Tianshi, Shen Haihua, Wang Pengyu, Pan Hong, IEEE Comp Soc. Fast Complete Memory Consistency Verification. HPCA-15 2009: FIFTEENTH INTERNATIONAL SYMPOSIUM ON HIGH-PERFORMANCE COMPUTER ARCHITECTURE, PROCEEDINGS. 2009, 第 2 作者381-+,
[22] Lv Yi, Lin Huimin, Pan Hong. Computing invariants for parameter abstraction. PROCEEDINGS - FIFTH ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, MEMOCODE07. 2007, 第 1 作者29-38, http://124.16.136.157/handle/311060/10950.
[23] 吕毅, 王源, 李晓林. 服务网格的用户3A使用模式. 电子学报[J]. 2007, 第 1 作者35(2): 292-298, http://lib.cqvip.com/Qikan/Article/Detail?id=23918923.
[24] Pan, Hong, Lin, HuiMin, Lv, Yi. Model checking data consistency for cache coherence protocols. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2006, 第 3 作者21(5): 765-775, https://www.webofscience.com/wos/woscc/full-record/WOS:000240962200014.
科研活动
科研项目
（ 1 ） 符号模型与隐式状态模型检测技术, 参与, 国家级, 2013-01--2016-12
（ 2 ） 同步数据流模型优化研究, 参与, 国家级, 2016-01--2019-12
（ 3 ） 限界正确性检查及相关模型检测技术, 参与, 国家级, 2017-01--2020-12
（ 2 ） 同步数据流模型优化研究, 参与, 国家级, 2016-01--2019-12
（ 3 ） 限界正确性检查及相关模型检测技术, 参与, 国家级, 2017-01--2020-12
参与会议
（1）Efficiently and Completely Verifying Synchronized Consistency Models Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, and Peng Wu 2014-11-05
（2）Finding Invariants for Parameter Abstraction 多核与异构并发计算学术研讨会 吕毅 2013-04-11
（2）Finding Invariants for Parameter Abstraction 多核与异构并发计算学术研讨会 吕毅 2013-04-11
指导学生
已指导学生
周琰 硕士研究生 081202-计算机软件与理论
孙鲁明 硕士研究生 081202-计算机软件与理论
赵晓凯 硕士研究生 081202-计算机软件与理论
熊浩军 硕士研究生 085211-计算机技术
李亮 硕士研究生 081202-计算机软件与理论