杨秋松是中国科学院软件研究所的研究员，其研究方向主要集中在软硬件模型检测与软硬件协同设计。他的研究成果获得了多项重要奖项，包括2025年国际计算机辅助验证会议（CAV）杰出论文奖和2010年国际软件工程会议（ICSE）ACM SIGSOFT杰出论文奖。他的论文涵盖以下几个主要方向：模型检测与形式化验证（例如IC3算法优化，包括深度优化IC3的SAT求解器、在IC3中每次SAT调用丢弃多个文字、预测IC3泛化中的引理，以及rIC3硬件模型检测器），参数化系统验证（例如参数化系统的有界验证和有界可达图），抽象与组合推理（例如通过抽象精化生成异步系统的假设），并行模型检测（例如Pregel中LTL模型检测的以顶点为中心的并行算法，以及LTL并行符号模型检测），处理器与硬件验证（例如用于处理器验证的重言式诱导通用属性、符号快速错误检测，以及硬件验证中符号执行的路径剪枝），以及计算机体系结构与微体系结构（例如硬件预取、存内计算模拟和安全推测执行）。

AI/LLM辅助的模型检测是他当前的研究重点。 他将大语言模型与形式化方法深度融合，致力于构建一个支持大规模系统验证的AI赋能体系，覆盖从问题分解、性质生成、引擎智能增强、子问题组合定理证明到智能符号执行的完整流程：利用LLM对复杂系统规范进行语义理解与自动分解，将大规模验证任务拆解为可管理的子问题；通过多模态规范提取自动生成硬件断言与验证性质，减少人工编写规范的成本；将AI能力嵌入模型检测引擎，例如智能优化SAT求解器与IC3算法中的引理预测与泛化过程；探索LLM辅助的子问题组合定理证明，自动生成证明策略与中间引理；并以错误语义为指导，结合符号合成与路径剪枝，实现RTL设计的自动修复与高效验证。这一体系旨在降低形式化验证对人工专家的依赖，推动AI与形式化方法的深度融合，从而支撑大规模复杂系统的可扩展验证。

欢迎对形式化方法、AI与系统验证交叉方向感兴趣的同学加入课题组，共同探索AI赋能大规模系统验证的前沿问题。也欢迎有志于软硬件协同设计与验证的同学联系交流。

   

083500-软件工程

软硬件深度融合，软件分析和系统安全，新型操作系统与系统安全

2006-09--2007-05   马萨诸塞州立大学阿姆赫斯特分校高级软件工程研究实验室   交流访问
2002-09--2008-07   中国科学院软件研究所   计算机软件与理论博士学位
1996-09--2000-06   中南大学   计算机科学与技术学士学位

2008--2010 中国科学院软件研究所            助理研究员

2010--2013  中国科学院软件研究所            副研究员

2011 -- 2012 卡耐基梅隆计算机学院 访问学者

2014--2024 中国科学院通用芯片与基础软件研究中心 研究员

2013-      中国科学院软件研究所            研究员

（1） 软件所优秀导师, , 研究所（学校）, 2026
（2） Distinguished Paper Award, 37th International Conference on Computer- Aided Verification, , 其他, 2025
（3） 中国科学院关键技术人才, 部委级, 2018
（4） 软件所优秀青年科技人才, , 研究所（学校）, 2013
（5） 北京市科学技术进步奖, 二等奖, 省级, 2012
（6） 创新促进会会员, 部委级, 2012
（7） ICSE Distinguished Paper Award, 其他, 2010
（8） ACM SIGSOFT Distinguished Paper Award, , 其他, 2010

[1] Xuhui Li, Yiyuan Zhang, Tianjun Bu, Qiusong Yang*, Fu Song and Zhilin Wu. Caster: Cost-Aware Selection of BTOR2 Verifiers. The 12th International Symposium on Dependable Software Engineering Theories, Tools and Applications, SETTA 2026.

[2] Tianjun Bu, Gaoyuan Zhou, Xuhui Li, and Qiusong Yang*. Bridging the indexing gap in fused gpu query engines. In 52nd International Conference on Very Large Data BasesBoston, MA, USA, 2026. Proceedings of the VLDB Endowment, 2026. CCF-A.

[3] 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.

[4] 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.

[5] 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.

[6] 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.

[7] 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.

[8] 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.

[9] 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.

[10] 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.

[11] 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. 

[12] 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.

[13] 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.

[14] 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.

[15] 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.

[16] 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.

[17] 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.

[18] 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.

[19] 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.

[20] 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.

[21] 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.

[22] 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.

[23] 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.

[23] 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.

[25] 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.

[26] 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.

[27] 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.

[28] 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.

[29] 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.

[30] 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.

[31] 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.

已指导学生

周鹏颖  硕士研究生  085212-软件工程  

乔若轩  硕士研究生  081202-计算机软件与理论  

王硕  硕士研究生  081203-计算机应用技术  

柴晓晨  硕士研究生  430113-软件工程  

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

张营飞  硕士研究生  083500-软件工程  

赵伟峰  硕士研究生  083500-软件工程  

刘欢  硕士研究生  081202-计算机软件与理论  

宋双洋  硕士研究生  083500-软件工程  

王玉庆  博士研究生  083500-软件工程  

石雯  硕士研究生  081202-计算机软件与理论  

张伟  硕士研究生  083500-软件工程  

时雨霖  硕士研究生  083500-软件工程  

张状  硕士研究生  085211-计算机技术  

金融通  硕士研究生  081202-计算机软件与理论  

杨超杰  硕士研究生  081202-计算机软件与理论  

杨昕昱  硕士研究生  081202-计算机软件与理论  

田天  硕士研究生  085212-软件工程  

冯馨玥  博士研究生  081202-计算机软件与理论  

梁佳辉  硕士研究生  085212-软件工程  

吕志超  博士研究生  083500-软件工程  

韩柔刚  硕士研究生  083500-软件工程  

戚航  硕士研究生  081202-计算机软件与理论  

蒋实知  博士研究生  081202-计算机软件与理论  

孙艺萱  硕士研究生  081200-计算机科学与技术  

李宇锋  博士研究生  083500-软件工程  

李蓥成  硕士研究生  081200-计算机科学与技术  

现指导学生

梁佳辉  博士研究生  081200-计算机科学与技术  

胡真  硕士研究生  081200-计算机科学与技术  

苏宇恒  博士研究生  081200-计算机科学与技术  

李林泽  硕士研究生  085405-软件工程  

田恩源  博士研究生  081200-计算机科学与技术  

李姝其  博士研究生  083500-软件工程  

卜天峻  硕士研究生  081200-计算机科学与技术  

漆楚衡  博士研究生  083500-软件工程  

李旭辉  硕士研究生  083500-软件工程