Speaker:

蔡少伟 (中科院软件研究所)

Time:

• 10:30-11:30 Beijing Time
• December 19, 2025 (Friday)

Venue:

B1-501, Main Building

Abstract:

布尔可满足性问题（SAT）是理论计算机的经典问题，同时有广泛的应用。SAT求解器是电子设计自动化（EDA）的重要基础引擎，尤其是现代EDA形式化验证技术的基础。本报告主要介绍我们在SAT求解器以及EDA形式化验证技术的研究进展。

Speaker Bio:

蔡少伟，中国科学院软件研究所研究员，中国科学院优秀导师，CCF杰出会员/学术工委执行委员，研究约束求解和形式化验证，主持自然基金委青年B项目和重点项目，获得领域顶级会议CAV、CP、SAT等会议的最佳/杰出论文奖，多次获得SAT比赛、SMT比赛和MaxSAT比赛冠军，以及鸿蒙创新大赛冠军等，担任SAT 会议程序委员会主席，受邀到SAT，CP，FMCAD等领域顶级会议做特邀报告。其求解器应用于包括华为、华大九天、中国航空集团、国家电网、阿里巴巴、微软等多家企业/机构在内的多个实际场景，包括集成电路验证、操作系统验证、云计算调度和航空制造调度等。