2020年11月30日上午，中国科学院软件研究所张健研究员应金沙威尼斯欢乐娱人城和符号计算与知识工程教育部重点实验室邀请，在金沙威尼斯欢乐娱人城中心校区计算机楼A521作了题为“计数与体积计算及程序分析”的学术报告。
张健，中国科学院软件研究所研究员。主要研究方向包括：自动推理、约束求解、软件测试与分析。目前担任《计算机学报》，JCST, Frontiers of CS, IEEE Trans. on Reliability,《中国科学：信息科学》，《计算机科学与探索》等刊物编委。曾先后获得中国科学院青年科学家奖、中创软件人才奖、国家杰出青年科学基金、国务院政府特殊津贴。
报告中，张健研究员首先用通俗易懂的数独游戏引出约束可满足问题，介绍了约束可满足问题、可满足性模理论问题的模型计数问题、模型计数和体积计算的应用领域尤其是在程序分析方面的应用。最后介绍了其团队在凸多面体整点个数估算上下界问题上的给出的方法，此方法比国际上最好的整点数计算工具快20倍以上，并且优势随着问题规模的增长而扩大，其相关源码也已公开发布到github上。最后，张健研究员悉心的回答到场同学的问题，本次报告受到了广大师生的热烈响应。
