时间：2026年4月25日（周六）19:00

参会方式：线上会议（可选择以下任意平台观看）

Bilibili直播：https://live.bilibili.com/25235207

腾讯会议：134-590-530

主办方：CCF系统软件专委会

主持人：王博（北京交通大学），陈俊洁（天津大学）

报告简介：本次分享会面向系统软件领域，邀请何静竹博士和王钟逸博士报告近期发表于OOSPLA上的工作，主题为软件安全与验证。

报告1：Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis

报告摘要：本文提出 Artemis，一种面向 PHP Web 应用 SSRF 漏洞检测的静态污点分析工具。它通过提取源与汇函数、构建显式和隐式调用图、结合规则约束的污点传播以及路径条件兼容性分析，提升了检测准确性并减少误报。实验表明，Artemis 在 250 个 PHP 应用中检测出 106 个真实 SSRF，仅产生 15 个误报，其中 35 个为新发现漏洞，24 个已获开发者确认并分配 CVE 编号。

报告人：何静竹博士现任上海科技大学信息科学与技术学院助理教授，2021 年于美国北卡罗来纳州立大学获得博士学位。她的研究方向聚焦于软件系统的可靠性与安全性，尤其致力于面向真实分布式系统设计自动化的检测、诊断与修复工具。

报告2：A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

报告摘要：本文提出 Preguss，一个结合静态分析、演绎验证与大语言模型的规约自动生成框架。其采用分而治之策略，首先根据证明目标（即潜在运行时错误断言）构建并排序验证单元，然后合成并精化单元级过程间规约，并保证可靠性与终止性。实验表明，Preguss 优于现有先进方法，可对千行以上工业程序实现高自动化内存安全验证，将人工验证工作量减少 80.6%–88.9%，并发现了某航天器控制软件中的 6 个真实运行时错误。

报告人：王钟逸，浙江大学计算机科学与技术学院博士生，导师是陈明帅研究员。主要研究方向是程序自动化验证与静态分析。相关研究成果发表于OOPSLA、ASE、J. Comput. Sci. Technol.等领域重要国际会议/期刊。