index_new5.html
../../../zaker_core/zaker_tpl_static/wap/tpl_guoji1.html
![]()
符号执行是形式化推理程序行为和检测软件漏洞的重要程序分析技术。然而，符号执行存在路径爆炸的固有局限性，当遇到数量庞大（程序大小的指数级）的路径时，传统的基于启发式权重的路径排序方法往往无法泛化到不同的程序。本次报告将介绍我们最近的工作Empc（S&P'25），一种用于符号执行的新型路径优先级技术。Empc计算路径覆盖，即可以覆盖所有代码块的最小路径子集，然后仅在该最小路径覆盖内进行搜索和调度，而不是在所有可能的路径中。通过减少路径搜索空间，Empc可以显著提高符号执行的性能。
😊Empc是一种用于符号执行的新型路径优先级技术，旨在解决路径爆炸问题，从而提高符号执行的性能。它通过计算路径覆盖，即可以覆盖所有代码块的最小路径子集，来减少路径搜索空间。
🔍Empc的核心思想是只搜索和调度路径覆盖内的路径，而不是所有可能的路径。这种方法可以显著减少需要探索的路径数量，从而提高符号执行的速度。
📈Empc通过减少路径搜索空间，可以显著提高符号执行的性能。这使得符号执行能够应用于更大的程序，并更有效地检测软件漏洞。
2025-08-09 19:43 上海
8月20日上午10:00，报告主题基于路径覆盖的符号执行路径优先探索策略，可腾讯会议线上参加
Novel Path Prioritization for Symbolic Execution
via Path Cover
摘要
Symbolic execution is an essential program analysis technique to formally reason program behaviors and detect software vulnerabilities. Despite its effectiveness, symbolic execution has an inherent limitation: path explosion. Path explosion occurs when symbolic execution encounters an overwhelming number (exponential to the program size) of paths. Traditional approaches rank the vast number of paths with heuristic-based weights. However, they often fail to be generalized to diverse programs. In this talk, I will introduce our recent work, Empc (S&P’25), a novel path prioritization technique for symbolic execution. We compute a path cover, i.e., a minimal subset of paths that can cover all code blocks, then only search and schedule within the minimal path cover instead of the vast number of all possible paths. By reducing the path search space, Empc can significantly boost symbolic execution performance.
报告人：佘东冬 助理教授，香港科技大学Dongdong She is an assistant professor at the Hong Kong University of Science and Technology, CSE department. He obtained his PhD from the CS department at Columbia University. Before Columbia, He earned his M.S. from UC Riverside and B.S. from Huazhong University of Science and Technology. He is broadly interested in security and machine learning. He is particularly interested in applying data-driven approaches (e.g., LLM, optimization) to solve traditional security problems (e.g., vulnerability detection, software testing, program analysis). His work has won distinguished paper awards in Oakland, ISSTA, best paper runner-up award in CCS and CSAW applied research award finalist.
活动安排
❖时间：2025年8月20日 上午10:00地点：复旦大学江湾校区交叉学科2号楼A2003
❖腾讯会议：会议号：593-840-767会议密码：585010阅读原文
跳转微信打开
