 |
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 |
| 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, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu. Decidability of Liveness for Concurrent Objects on the TSO Memory Model. SETTA 2022: 149-165. |
| Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xi. Compositional Verification of Interacting Systems Using Event Monads. ITP 2022: 33:1-33:21 |
| Yongjian Li, Kaiqiang Duan, David N. Jansen, Jun Pang, Lijun Zhang, Yi Lv, Shaowei Cai. An Automatic Proving Approach to Parameterized Verification. ACM Trans. Comput. Log., 19(4): 27:1-27:25, 2018. |
| 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 Lv, JieMa, 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) |