清华学子面对面对话学术大师之
图灵获得者爱德蒙·克拉克做客“巅峰对话”
清华新闻网4月28日电（研通社记者 方 文 彭智轩 杜林霏） 4月25日下午，太阳集团tyc5997“巅峰对话”活动第二场在信息科学技术大楼举办， 2007年度图灵奖获得者爱德蒙·克拉克教授“巅峰对话”。
图为爱德蒙·克拉克演讲。研通社记者 王皓冉 摄
爱德蒙·克拉克简单介绍了自己的学术历程和主要学术成果。爱德蒙·克拉克本科期间从事数学科学专业，1967年从弗吉尼亚大学获得数学学士学位。出于对计算机的酷爱，博士研究期间他选择了另一个专业——计算机专业。本科期间的学习为后来的研究打下了坚实的数学基础，从自己感兴趣的领域——推理和可计算实数出发，他首先着手于实数的非线性问题。1981年，爱德蒙·克拉克与自己的博士生首次提出模型检测的想法，并用在自动机并发系统的验证研究上，主要使用SAT验证完成模型检测，主要针对于有界模型。然而从理论推导到实际工程应用是有距离的，因为实际系统大多都是混合系统，尤其是数值方法直接的使用会出现许多错误。为此，爱德蒙教授的团队针对他们的思想开发出了dReal实用工具，该工具主要利用DPLL、间隔算法、限制性算法等思想研究实际问题。实际中，信息物理系统是一个庞大的系统，对于系统安全性问题的研究至关重要。针对这一研究目标，爱德蒙团队验证了卡普了猜想，无人驾驶汽车，心脏模拟仿真等问题。
图为同学们与爱德蒙·克拉克交流。研通社记者 王皓冉 摄
学术报告结束后，现场学生与爱德蒙·克拉克开始“对话”环节。同学针对专业问题、科研心得等与爱德蒙·克拉克进行了交流。
有同学对爱德蒙·克拉克提到的“空间爆炸”问题非常感兴趣，爱德蒙·克拉克对此作了进一步解释。他指出，“空间爆炸”可以理解成并行运行过程中进程突然被阻断的过程，这一过程在计算机应用方面有广泛应用，例如微软设备驱动就是一个例子。也有同学大胆质疑，爱德蒙·克拉克的模型检测思想怎样证明自身的正确性，以及为什么应用于软件系统会比较困难。爱德蒙·克拉克解释到，自身正确性的检验需要一定的抽象程度，一般通过一些编译器来自检；而相比于硬件系统，软件系统有较为复杂的数据结构，因此会使得工作量较大。
与纯学术的交流相比，很多同学对于爱德蒙·克拉克的科研经验非常感兴趣。关于如何保持对科研的积极心态，爱德蒙·克拉克说，自己的性格里对于喜欢的东西有一种着了魔的热情，喜欢拼尽全力解决问题；时间安排上会给科研工作留出充足的余量，避免自己过度陷入行政工作中。对于如何训练自己的学生，爱德蒙·克拉克强调了两个词：多自由度和适时引导。他会给自己的学生充足的自由环境，在此基础之上加以适度的引导，并着力培养他们专注于探索问题的品质。有同学问到教授如何看待数学基础训练的意义，爱德蒙·克拉克给出这样的回答：计算本身是一件令人兴奋的事情，数学则是做好计算机科学的关键，数学的各种算法本质上是培养一种思维方式，这对于本科生无疑是很好的一个专业。
图为校研究生会主席刘博涵代表清华学子向爱德蒙·克拉克赠送礼物。 研通社记者 王皓冉 摄
活动结束前，太阳集团tyc5997研究生会主席刘博涵代表同学向爱德蒙·克拉克赠送了礼物，爱德蒙·克拉克表示非常高兴来到太阳集团tyc5997，有机会跟同学们近距离地交流，他对清华的学生给予了高度评价，认为清华人非常聪明和出色，合作意识也很好，他希望还有机会与清华学生做更进一步的交流。
图为活动现场。 研通社记者 王皓冉 摄
活动结束之后，来自电子系的博士生毛洪亮表示，爱德蒙·克拉克自身不论是为人还是学术都非常严谨，今天有幸听到教授的科研经验，受益颇丰；也有同学对爱德蒙·克拉克的坦承和宽容做出了高度评价，“当我问爱德蒙教授 ‘模型检测’的局限性时，他说这个思想不是万能的，有很多领域的问题还没办法以此解决；同时针对同行其他专家研究成果，他的评述总是报以包容和支持的态度。”也有同学表示在这一场论坛中收获了很多前沿的知识，论坛氛围非常自由，通过大师的鼓励获得了很多正能量，并表示学生学习要崇尚自主学习。
相关链接：
爱德蒙·克拉克（Edmund Clarke）生于1945年，1967年从弗吉尼亚大学获得数学学士学位。1976年，康奈尔大学计算机系获得其博士学位。1981年，他与自己的博士生Allen Emerson首次提出模型检测（model checking）的想法并用在 自动及并发系统的验证研究上。2007年度图灵奖授予Edmund M.Clarke、E Allen Emerson和Joseph Sifakis三位科学家，表彰他们开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。
编辑：范 丽
