​Hardware/software model checking, hardware/software codesign

2000 BS (Computer Science and Technology),Central South University.
2008 PhD (Computer Software and Theories),Institute of Software, Chinese Academy of Sciences.

​2006-2007  Exchange Student, Laboratory for Advanced Software Engineering Research, UMass Amherst  

2008-2010  Assistant Research Professor, Institute of Software, Chinese Academy of Sciences

2010-2013  Associate Research Professor, Institute of Software, Chinese Academy of Sciences 

2011-2012   Visiting Scholar, Computer Sciences Department, Carnegie Mellon University

2013-         Research Professor, Institute of Software, Chinese Academy of Sciences

2014-         Research Professor, CPU and Fundamental Software Research Center, Chinese Academy of Sciences

​2025 Distinguished Paper Award, 37th International Conference on Computer-Aided Verification

2010  ACM SIGSOFT Distinguished Paper Award, the 32nd ACM/IEEE International Conference
on Software Engineering

[1] Tianjun Bu, Zhichao Lyu, Qiusong Yang*. Dropping Multiple Literals per SAT call in IC3 Model Checking. In Proceedings of the 63st ACM/IEEE Design Automation Conference, DAC 2026, Long Beach CA, USA, July 26-29, 2026. CCF-A.

[2] Enyuan Tian, Yiwei Ci, Qiusong Yang*, Yufeng Li, and Zhichao Lyu. S3-repair: Error-semantic guided symbolic synthesis for RTL repair. In 29th International Conference on Computer Supported Cooperative Work in Design, Fuzhou, China, from May 13-15, 2026, Lecture Notes in Computer Science. Springer, 2026.

[3] Jiahui Liang, Qiusong Yang*, and Yiwei Ci. Dataflow-based path pruning in symbolic execution for hardware verification. In 29th International Conference on Computer Supported Cooperative Work in Design, Fuzhou, China from May 13-15, 2026, Lecture Notes in Computer Science. Springer, 2026.

[4] Keqin Sun, Qiusong Yang, and Mingshu Li. ChipKDRAG: Knowledge-driven multi-agent RAG framework for digital chip placement. In 29th International Conference on Computer Supported Cooperative Work in Design, Fuzhou, China from May 13-15, 2026, Lecture Notes in Computer Science. Springer, 2026.

[5] Keqin Sun, Qiusong Yang, and Mingshu Li. Chiphier: A partitioning and optimization framework for large-scale chip design. In 29th International Conference on Computer Supported Cooperative Work in Design, Fuzhou, China from May 13-15, 2026, Lecture Notes in Computer Science. Springer, 2026.

[6] Enyuan Tian, Yiwei Ci, Qiusong Yang*, Yufeng Li, and Zhichao Lyu. Assert-synth:LLM-based assertion synthesis via multimodal specification extraction. In lEEE International Symposium on Circuits and Systems, Shanghai, China from May 24-27, 2026, Lecture Notes in Computer Science. Springer, 2026.

[7] Xinmin Zheng, Mingshu Li, Qiusong Yang, and Wenbo Li. Formal verification of a crash-safe file system based on non-persistent conditions extended concurrent separation logic. In 2025 IEEE 31th International Conference on Parallel and Distributed Systems (ICPADS), pages 1–9, 2025.

[8] Keqin Sun, Qiusong Yang, and Mingshu Li. ChipDRAG: Dynamic RAG for chip placement. In Proceedings of the 25th International Conference on Algorithms and Architectures for Parallel Processing, IC3APP 2025, Zhengzhou, Henan, China, October 30 - Novermber 02, 2025. IEEE, 2025.

[9] Zhichao Lv, Tianjun Bu, Qiusong yang*. Fast, Transparent and Accurate Simulation of Thousand Processing-in-Memory Cores. 35th edition of Great Lakes Symposium on VLSI, GLSVLSI 2025. 

[10] Yufeng Li, Yiwei Ci, Qiusong Yang, and Enyuan Tian. Efficient processor verification by tautologies-derived universal properties model checking. Integration, the VLSI journal, 105:102502, 2025.

[11] Yuheng Su, Qiusong Yang*, Yiwei Ci, Yingcheng Li, Tianjun Bu, and Ziyu Huang. Deeply optimizing the SAT solver for the IC3 algorithm. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 21-25, 2025, Lecture Notes in Computer Science. Springer, 2025. CCF-A.

[12] Yuheng Su, Qiusong Yang*, Yiwei Ci, Tianjun Bu, and Ziyu Huang. The rIC3 hardware model checker. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 21-25, 2025, Lecture Notes in Computer Science. Springer, 2025. CCF-A. Distinguished Paper Award.

[13] Yuheng Su, Yingcheng Li, Qiusong Yang*, Yiwei Ci, and Ziyu Huang. Property-driven parallel symbolic model checking of LTL. In Proceedings of the 62st ACM/IEEE Design Automation Conference, DAC 2025, Moscone West, San Francisco CA, USA, June 22-26, 2025. ACM, 2025. CCF-A.

[14] Yuheng Su, Qiusong Yang*, and Yiwei Ci. Predicting lemmas in generalization of IC3. In Vivek De, editor, Proceedings of the 61st ACM/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, June 23-27, 2024, pages 208:1– 208:6. ACM, 2024. CCF-A.

[15] Yufeng Li, Qiusong Yang*, Yiwei Ci, and Enyuan Tian. SEPE-SQED: symbolic quick error detection by semantically equivalent program execution. In Vivek De, editor, Proceedings of the 61st ACM/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, June 23-27, 2024, pages 258:1–258:6. ACM, 2024. CCF-A.

[16] Yufeng Li, Yiwei Ci, and Qiusong Yang*. TIUP: effective processor verification with tautology-induced universal properties. In Proceedings of the 29th Asia and South Pacific Design Automation Conference, ASPDAC 2024, Incheon, Korea, January 22-25, 2024, pages 269–274. IEEE, 2024.

[17] Xiaoni Meng, Qiusong Yang, Yiwei Ci, Pei Zhao, Shan Zhao, and Mingshu Li. Execute on clear (eoc): Enhancing security for unsafe speculative instructions by precise identification and safe execution. In 41st IEEE International Conference on Computer Design, ICCD 2023, Washington, DC, USA, November 6-8, 2023, pages 587–595. IEEE, 2023.

[18] Shizhi Jiang, Qiusong Yang*, and Yiwei Ci. Merging similar patterns for hardware prefetching. In 55th IEEE/ACM International Symposium on Microarchitecture, MICRO 2022, Chicago, IL, USA, October 1-5, 2022, pages 1012–1026. IEEE, 2022. CCF-A.

[19] Xiaoni Meng, Qiusong Yang, Yiwei Ci, Pei Zhao, Shan Zhao, Tianlin Huo, and Mingshu Li. Secure access policy (SAP): Invisibly executing speculative unsafe accesses in an isolated environment. In 2022 IEEE 40th International Conference on Computer Design (ICCD), pages 80–88, Los Alamitos, CA, USA, oct 2022. IEEE Computer Society.

[20] Shizhi Jiang, Yiwei Ci, Qiusong Yang*, and Mingshu Li. Matryoshka: A coalesced delta sequence prefetcher. In Xian-He Sun, Sameer Shende, Laxmikant V. Kalé, and Yong Chen, editors, ICPP 2021: 50th International Conference on Parallel Processing, Lemont, IL, USA, August 9 - 12, 2021, pages 5:1–5:11. ACM, 2021.

[21] Xinyue Feng, Qiusong Yang*, Lin Shi, and Qing Wang. Behaviorki: Behavior pattern based runtime integrity checking for operating system kernel. In 2018 IEEE International Conference on Software Quality, Reliability and Security, QRS 2018, Lisbon, Portugal, July 16-20, 2018, pages 13–24. IEEE, 2018.

[22] Yuqi Lin, Saif Ur Rehman Malik, Kashif Bilal, Qiusong Yang, Yongji Wang, and Samee U. Khan. Designing and modeling of covert channels in operating systems. IEEE Trans. Computers, 65(6):1706–1719, 2016.

[23] Miao Xie, Qiusong Yang, Qing Wang, Gao Cong, and Gerard de Melo. Dynadiffuse: A dynamic diffusion model for continuous time constrained influence maximization. In Blai Bonet and Sven Koenig, editors, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pages 346–352. AAAI Press, 2015. CCF-A.

[24] Miao Xie, Qiusong Yang, Jian Zhai, and Qing Wang. A vertex centric parallel algorithm for linear temporal logic model checking in pregel. J. Parallel Distributed Comput., 74(11):3161–3174, 2014.

[25] Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, and Mingshu Li. Assumption generation for asynchronous systems by abstraction refinement. In Corina S. Pasareanu and Gwen Salaün, editors, Formal Aspects of Component Software, 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers, volume 7684 of Lecture Notes in Computer Science, pages 260–276. Springer, 2012.

[26] Qiusong Yang, Bei Zhang, Jian Zhai, and Mingshu Li. Attacking the dimensionality problem of parameterized systems via bounded reachability graphs. In Farhad Arbab and Marjan Sirjani, editors, Fundamentals of Software Engineering - 4th IPM International Conference, FSEN 2011, Tehran, Iran, April 20-22, 2011, Revised Se- lected Papers, volume 7141 of Lecture Notes in Computer Science, pages 221–235. Springer, 2011.

[27] Qiusong Yang and Mingshu Li. A cut-off approach for bounded verification of parameterized systems. In Jeff Kramer, Judith Bishop, Premkumar T. Devanbu, and Sebastián Uchitel, editors, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pages 345–354. ACM, 2010. CCF-A. ACM SIGSOFT Distinguished Paper Award.

[28] Qiusong Yang, Mingshu Li, Qing Wang, Guowei Yang, Jian Zhai, Juan Li, Lishan Hou, and Yun Yang. An algebraic approach for managing inconsistencies in software processes,. In Qing Wang, Dietmar Pfahl, and David M. Raffo, editors, Software Process Dynamics and Agility, International Conference on Software Process, ICSP 2007, Minneapolis, MN, USA, May 19-20, 2007, Proceedings, volume 4470 of Lecture Notes in Computer Science, pages 121–133. Springer, 2007.

[29] Mingshu Li, Qiusong Yang, Jian Zhai, and Guowei Yang. On mobility of software processes. In Qing Wang, Dietmar Pfahl, David M. Raffo, and Paul Wernick, editors, Software Process Change, International Software Process Workshop and Inter- national Workshop on Software Process Simulation and Modeling, SPW/ProSim 2006, Shanghai, China, May 20-21, 2006, Proceedings, volume 3966 of Lecture Notes in Computer Science, pages 105–114. Springer, 2006.