基本信息
吕毅  男  硕导  中国科学院软件研究所
电子邮件: lvyi@ios.ac.cn
通信地址: 中科院软件所计算机科学国家重点实验室
邮政编码: 100190

招生信息

   
招生专业
081202-计算机软件与理论
085400-电子信息
招生方向
网络与并发实时系统的设计与分析
形式验证
模型检测

教育背景

2000-09--2004-07   中国科学院计算技术研究所   获博士学位
1997-09--2000-07   中国科学院计算技术研究所   获硕士学位
1989-09--1993-07   电子科技大学   获学士学位

工作经历

   
工作简历
2009-01~现在, 中国科学院软件研究所, 副研究员
2007-02~2008-12,中国科学院软件研究所, 助理研究员
2004-08~2007-01,中国科学院软件研究所, 博士后
1993-08~1997-08,南京电子技术研究所, 助理工程师

教授课程

并发数据结构与多核编程
多处理器系统编程

出版信息

   
发表论文
[1] 王超, 吕毅, 吴鹏, 贾巧雯. TSO 内存模型下限界可线性化的可判定性研究. 软件学报[J]. 2022, 33(8): 2896-2917, [2] 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)null. 2022, [3] Wang, Chao, Lv, Yi, Wu, Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2018, 61(1): https://www.webofscience.com/wos/woscc/full-record/WOS:000409915100006.
[4] 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, 19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.
[5] Wang, Chao, Lv, Yi, Wu, Peng. TSO-to-TSO linearizability is undecidable. ACTA INFORMATICA[J]. 2018, 55(8): 649-668, https://www.webofscience.com/wos/woscc/full-record/WOS:000452106900003.
[6] 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 SCIENCEnull. 2017, 10139: 188-202, [7] Wang Chao, Lv Yi, Wu Peng. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2017, 61(1): [8] 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)null. 2016, 560-567, [9] 吕毅. Bounded TSO-to-SC Linearizability is Decidable. SOFSEM2016. 2016, [10] 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)null. 2016, 111-121, http://dx.doi.org/10.1109/ICECCS.2016.12.
[11] 吕毅. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols. ATVA2015. 2015, [12] Wang Chao, Lv Yi, Liu Gaoang, Wu Peng, Feng X, Park S. Quasi-Linearizability is Undecidable. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015null. 2015, 9458: 369-386, [13] 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)null. 2015, 246-253, [14] 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 2015null. 2015, 9364: 309-325, [15] 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 2014null. 2014, 8837: 264-280, [16] 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, PROCEEDINGSnull. 2009, 5477: 143-+, [17] Pan Hong, 吕毅, 林惠民. Environment abstraction with state clustering and parameter truncating. Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009null. 2009, http://124.16.136.157/handle/311060/8304.
[18] 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, PROCEEDINGSnull. 2009, 381-+, [19] 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, MEMOCODE07null. 2007, 29-38, http://124.16.136.157/handle/311060/10950.
[20] 吕毅, 王源, 李晓林. 服务网格的用户3A使用模式. 电子学报[J]. 2007, 35(2): 292-298, http://lib.cqvip.com/Qikan/Article/Detail?id=23918923.

科研活动

   
科研项目
( 1 ) 符号模型与隐式状态模型检测技术, 参与, 国家级, 2013-01--2016-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

指导学生

已指导学生

周琰  硕士研究生  081202-计算机软件与理论  

孙鲁明  硕士研究生  081202-计算机软件与理论  

赵晓凯  硕士研究生  081202-计算机软件与理论  

熊浩军  硕士研究生  085211-计算机技术  

李亮  硕士研究生  081202-计算机软件与理论