Yi LÜ (Yi Lv)             中文版

    I am an associate research professor at State Key Laboratory of  Computer Science, Institute of Software, Chinese Academy of Sciences,  researching on formal verification and model checking. 

P.O.Box 8718
Beijing 100190
P.R.China
Email: lvyi(at)ios.ac.cn

 

Education
2000.9-2004.7:Received Ph.D. in Computer Architecture at National Research Center for Intelligent Computing Systems Institute of Computing Technology, Chinese Academy of Sciences.
1997.9-2000.7:Received M.S. in Computer Application at Institute of Computing Technology, Chinese Academy of Sciences.
1989.9-1993.7:Received B.S. in Electronic Precision Machine at University of Electronic Science and Technology of China.
Experience
2009.1-now:associate research professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
2007.2-2009.1:assistant research professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
2004.8-2007.2:postdoc at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
1993.8-1997.7:assistant engineer at Nanjing Research Institute of Electronics Technology
Publications
Chao Wang, Yi Lv, Peng Wu. Decidability of Linearizabilities for Relaxed Data Structures. SCIENCE CHINA Information Sciences, 61(012103): 1-10, 2018. Springer.
Chao Wang, Yi Lv, Peng Wu. TSO-to-TSO Linearizability is Undecidable. Acta Informatica, 2017. Published Online. Springer. https://doi.org/10.1007/s00236-017-0305-6
Chao Wang, Yi Lv, Peng Wu. Decomposable Relaxation for Concurrent Data Structures. The 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), 2017.
Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang, Shaowei Cai. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. The 34th IEEE International Conference on Computer Design (ICCD), 2016.
Wei Ji, Farn Wang, Peng Wu, Yi Lv. An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata. The 21st International Conference on Engineering of Complex Computer Systems (ICECCS), 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. pdf
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. [Report Version]
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. [Report Version]
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. pdf
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. pdf
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. pdf
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 LvJieMa,  RongfengTang. 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 & Computer Graphics, 2001, Vol.13, No.6 (in Chinese)
Tools
PaMC : A Parameterized Model Checker
MODV : A Fast Memory Consistency Model Dynamic Verifier