10月30日 Moshe Y. Vardi:Program Verification——a 50-Year History


报告人信息:

Moshe Y. Vardi is University Professor, Karen Ostrum George Distinguished Service Professor in Computational Engineering, and Director of the Ken Kennedy Institute for Information Technology at Rice University. His interests focus on automated reasoning, a branch of Artificial Intelligence with broad applications to computer science, including machine learning, database theory, computational-complexity theory, knowledge in multi-agent systems, computer-aided verification, and teaching logic across the curriculum.



报告摘要:

  2019年是托尼·霍尔爵士发表CACM论文“计算机编程的公理基础” 五十周年。在那篇论文中,托尼·霍尔爵士说:“一个程序的正确性,当它的编译器和计算机硬件都具有数学确定性时,将有可能很大程度上依赖于程序的结果,且仅通过电子元器件的可靠性的限制来预测它们的属性。”

  在这次演讲中,我将回顾这一愿景50年的历史,描述障碍、争议和进展里程碑。最后,我将描述过去几年中取得的令人印象深刻的进展和戏剧性的失败。






扑克21公式