下载中心
会议室预定
电子邮箱
最优化模理论及其程序分析应用
| Title: | 最优化模理论及其程序分析应用 |
| Speaker: | 姚培森（研究员，浙江大学） |
| Time: | 2024年11月22日 (周五) 10:00-11:30 |
| Venue: | 线下：中国科学院软件园区5号楼三层 334会议室 线上：腾讯会议：816-633-676 |
| Abstract: | 最优化模理论(Optimization Modulo Theory,OMT)是可满足模理论(Satisfiability Modulo Theory,SMT)的扩展:给定约束条件P 和目标函数 f,寻找 P 的可满足解，使得 f的值最大或最小化OMT 在程序分析与验证中具有重要应用，例如最优抽象解释WCET 分析等。目前OMT 求解主要包括两类方法:一是将 OMT 转化为其他自动推理问题(如最大可满足性、量词实例化等);二是基于 SMT 的迭代优化算法(如线性搜索、二分搜索等)。OptiMathSAT 和 Z3 等求解器均支持 OMT约束求解，但在处理复杂约束时，现有方法仍面临性能瓶颈。本报告主要分享针对位向量约束的OMT问题，我们近期的相关串行和并行算法，及其在二进制静态分析、混合模糊测试等场景的应用。 |
| Bio: | 姚培森，浙江大学“百人计划”研究员，CCF形式化方法专委、理论计算机科学专委执行委员，ACM SIGPLAN、SIGSAC会员，研究方向为编程语言(程序分析与验证、程序合成与优化)，数理逻辑(自动定理证明)，软件安全(洞挖掘)。相关成果发表于编程语言(PLDI，00PSLA)、软件工程(ICSEESEC/FSE, ISSTA, ASE, TOSEM)、信息安全(IEEE S&P, USENIX SecurityTDSC)、计算机系统(ASPLOS)等领域的CCF-A会议或期刊，获ACM SIGPLAN杰出论文奖、ACM SIGSOFT杰出论文奖、Google Research Paper Rewards等奖项担任相关领域顶级会议(POPL 25，00PSLA 25,ISSTA 24,CCS 24，PLDI 23)程序委员会委员。 |