General

Yi Lv Associate Professor
Email: lvyi@ios.ac.cn 
Telephone: 010-62661658
Address: State Key Laboratory of Computer Science,Institute of Software

Postcode: 100190 

Research Areas

formal verification, concurrency theory, parameterized model checking, automatic verification and analysis of concurrent programs


Education

Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China. Ph.D., Computer Architecture, May 2004

Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China. M.S., Computer Applications, May 2000

University of Electronic Science and Technology of China, Chengdu, China. B.A., Electronic Precision Machine,  May, 1993

Experience

   
Work Experience

2015 Jan. - Present. Associate Professor. School of Computer and Control Engineering, University of Chinese Academy of Sciences, Beijing, China

2009 Jan. - Present. Associate Researcher. State Key Laboratory of Computer Science, Institute of Software,

Chinese Academy of Sciences, Beijing, China

2007 Feb. - 2009 Jan. Assistant Researcher. State Key Laboratory of Computer Science, Institute of Software,

Chinese Academy of Sciences, Beijing, China

2004 Aug. - 2007 Feb. Postdoc. State Key Laboratory of Computer Science, Institute of Software,

Chinese Academy of Sciences, Beijing, China

1993 Aug. - 1997 Jul. Assistant Engineer. Nanjing Research Institute of Electronics Technology, Nanjing, China

Teaching Experience

2015-2016 091M5026H Concurrent Data Structures and Multicore Programming 

2016-2017 091M5026H Concurrent Data Structures and Multicore Programming 

Publications

Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang, and Shaowei Cai. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. The 34th IEEE International Conference on Computer Design (ICCD), 2016.

Chao Wang, Yi Lv, and Peng Wu. Bounded TSO-to-SC Linearizability is Decidable. The 42nd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), 2016.

Han Yue, Peng Wu, Tsong-Yueh Chen and Yi Lv. Input-driven Active Testing of Multi-threaded Programs. The 22nd Asia-Pacific Software Engineering Conference (APSEC), 2015.

Chao Wang, Yi Lv, Gaoang Liu, and Peng Wu. Quasi-Linearizability is Undecidable. The 13th Asian Symposium on Programming Languages and Systems (APLAS), 2015.

Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao and Kaiqiang Duan. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols. The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2015.

Chao Wang, Yi Lv and Peng Wu. TSO-to-TSO Linearizability is Undecidable. The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2015.

Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, and Peng Wu. Efficiently and Completely Verifying Synchronized Consistency Models. The 12th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2014.

Yunji Chen, Yi Lv, Weiwu Hu, Tianshi Chen, Haihua Shen, Pengyu Wang, and Hong Pan. Fast Complete Memory Consistency Verification. The 15th International Symposium on High-Performance Computer Architecture (HPCA), 2009.

Hong Pan, Yi Lv, and Huimin Lin. Environment Abstraction with State Clustering and Parameter Truncating. Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), 2009.

Yi Lv, Huimin Lin, and Hong Pan. Computing Invariants for Parameter Abstraction. Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2007.

Yi Lu, Yuan Wang, Xiao-lin Li. 3A Utilization Mode of Service Grid. Acta Electronica Sinica, 2007, Vol.35, No.2 (in Chinese)

Hong Pan, Huimin Lin, and Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols. Journal of Computer Science and Technology, 2006, Vol.21, No.5.

Yi Lv,  Jie Ma,  Rongfeng Tang. FSbench: A General Cluster File System Benchmark. Computer Engineering, 2004, Vol.30, No.2 (in Chinese)

Jin He, Jin Xiong, Sining Wu, Yi Lu, Dan Meng. DCFS: File Service in Commodity Cluster Dawning 4000. In Proceedings of the Fourth International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), 2003.

Yi Lu, Zhi-Jiang Yao,  Dao-Zheng Wei, Yong-Liang Xie. An OBDD Method for Analysis of Asynchronous Sequential Circuits, Journal of Computer-Aided Design and Computer Graphics, 2001, Vol.13, No.6 (in Chinese)

Students

已指导学生

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

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

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

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

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