计算机与软件工程学院学术报告——SAT求解及EDA形式化技术简述

报告题目：SAT求解及EDA形式化技术简述

主讲人：张昕荻 博士（中国科学院软件研究所）

报告时间：2025年12月19日（周五）14:30—17:00

报告地点：西华大学6A-509

主办单位：计算机与软件工程学院

主讲人简介：

张昕荻，中国科学院软件研究所，中科院特别研究助理，主要研究方向为约束求解及形式化验证，于SAT、CAV、DAC、ICSE等会议及期刊发表学术论文20余篇。其研究工作获评国际SAT协会“最佳博士学位论文奖”（中国首个）、国际SAT会议“最佳论文奖”（中国首个）、中国科学院优秀博士学位论文等。其研制的求解器曾于国际SAT、SMT、FLoC比赛夺冠20余次，相关技术落地于国内多家头部EDA企业，并应用于密码分析领域，获“强网杯”密码数学专项赛全国冠军。他曾获中科院院长奖特别奖等荣誉，并获中国教育发展基金会“奋进奖学金--集成电路人才培养”专项资助。主持或参与国自然青年基金、中科院战略先导A、国自然重点、国家重点研发等课题。

内容简介：

可满足性问题（SAT）是计算机科学的核心问题，SAT求解技术作为关键的形式化方法，在“卡脖子”电子设计自动化（EDA）领域具有重要应用价值，已成为形式化验证与测试生成的核心计算引擎。随着问题规模与复杂度的持续增长，SAT求解器面临显著的性能瓶颈。报告从两个方面展开：一是从求解器层面，介绍SAT参数配置、定制求解、并行算法的若干探索与实践；二是在应用层面，讨论相关SAT求解技术在组合等价性验证（CEC）、自动测试向量生成（ATPG）等EDA关键问题中的定制策略与并行求解应用技术。 

报告人照片：