报告题目：定理证明自动化：历史、现状、未来
报告摘要：定理证明自动化是人类长期以来的一个梦想，推动了计算机科学的诞生，是形式化方法的核心问题。本报告对定理证明自动化的历史进行回顾，对现状进行总结，对未来进行展望。
报告人简介：吴志林，中国科学院软件研究所基础软件与系统重点研究员，博士生导师， 2020年“CCF-IEEE CS”青年科学家奖获得者。长期从事计算逻辑、自动机理论、计算机软硬件系统形式验证相关的研究，在知名国际会议和期刊上发表论文40余篇，包括LICS、POPL、CAV、DAC等。先后主持多项国家级项目，包括国家重点研发计划课题、中科院先导A项目课题、“十三五”全军共用信息系统装备预先研究项目、国家自然科学基金面上基金等。中国计算机学会形式化方法专业委员会秘书长，国际会议ATVA 2022、TASE 2025程序委员会共同主席，CAV、CONCUR、ATVA等国际会议的程序委员会委员。
报告时间：2025年6月6日14:30
报告地点：数学与统计学院四楼会议室
主办单位：湖北民族大学数学与统计学院
联系人：孙全
欢迎广大师生参加！