2020年11月30日上午，中國科學院軟件研究所張健研究員應伟德国际BETVlCTOR和符号計算與知識工程教育部重點實驗室邀請，在伟德国际BETVlCTOR中心校區計算機樓A521作了題為“計數與體積計算及程序分析”的學術報告。
張健，中國科學院軟件研究所研究員。主要研究方向包括：自動推理、約束求解、軟件測試與分析。目前擔任《計算機學報》，JCST, Frontiers of CS, IEEE Trans. on Reliability,《中國科學：信息科學》，《計算機科學與探索》等刊物編委。曾先後獲得中國科學院青年科學家獎、中創軟件人才獎、國家傑出青年科學基金、國務院政府特殊津貼。
報告中，張健研究員首先用通俗易懂的數獨遊戲引出約束可滿足問題，介紹了約束可滿足問題、可滿足性模理論問題的模型計數問題、模型計數和體積計算的應用領域尤其是在程序分析方面的應用。最後介紹了其團隊在凸多面體整點個數估算上下界問題上的給出的方法，此方法比國際上最好的整點數計算工具快20倍以上，并且優勢随着問題規模的增長而擴大，其相關源碼也已公開發布到github上。最後，張健研究員悉心的回答到場同學的問題，本次報告受到了廣大師生的熱烈響應。
