题目：约束求解与自动推理
报告人：张健
中国科学院软件研究所研究员
国家杰出青年科学基金获得者
地点：计算机学院101会议室
时间：2017年12月22日（周五）上午10:00
报告摘要：约束求解与自动推理是人工智能的重要研究方向。本报告将介绍此方向和相关领域的基本情况，以及我们的一些研究内容及成果。包括：约束条件和逻辑公式的可满足性判定，复杂约束条件的解空间大小的计算，数学问题求解，程序分析等。
报告人简介：张健，中国科学院软件研究所研究员。主要研究兴趣包括：自动推理和约束求解算法，程序静态分析和软件测试技术。曾先后获得中创软件人才奖、国家杰出青年科学基金、国务院政府特殊津贴。担任《计算机学报》、《中国科学：信息科学》、Journal of Computer Science and Technology、Frontiers of Computer Science、IEEE Transactions on Reliability、《计算机科学与探索》编委。曾担任ICSE、VSTTE、IJCAR、CADE、SAT、COMPSAC等重要国际会议程序委员会委员以及国际会议QRS 2015程序委员会主席。