3月15、16两天，由我院主办、中欧联合实验室（LIAMA，北京）协办、学院软件理论与系统所承办的第二届“清华软件日”软件理论学术论坛在FIT大楼举行。今年的会议主题是“工业级验证”。

15日，5位在形式化方法基础研究中做过开创性工作，同时又在软硬件的工业级可信性验证方面取得杰出成就的国际一流学者做了特邀报告。巴黎高等师范学院的Patrick Cousot教授是“抽象解释”理论的创立人，他介绍了抽象解释在大规模软件验证中的应用技术及当前研究热点。Intel公司资深软件工程师、浮点算法及算术逻辑电路正确性验证专家John Harrison介绍了Intel采用的形式化验证技术谱系及成功经验。澳大利亚新南威尔士大学John Lions操作系统讲习教授Gernot Heiser，曾荣获2009新南威尔士州“年度科学家”及“创新英雄”等荣誉，其领导开发的OKL4实时操作系统商业产品在嵌入式设备上的应用已超过15亿套。Gernot Heiser与澳大利亚信息通信技术研究中心首席科学家Gerwin Klein领导的定理证明团队合作，于2009年首次完成了一个工业级操作系统微内核seL4的完整功能性验证，在学术界和工业界均引起了广泛反响。他们分别介绍了嵌入式软件可信性面临的挑战和机遇，以及操作系统信息安全验证技术与挑战。Vocera Communications公司创始人、首席技术官Rob Shostak的报告掀起了当天活动的一个小高潮。Shostak早年ZQ从事软件理论基础研究，后基于其自己发明的技术创业，在科研和商业上都取得了丰硕成果。他发明了一种基于重写（一种可计算性理论模型）的语音识别技术，基于该技术设计的全语音控制近距离无线通信设备面向医院等行业及生活应用销售量达到几十万套，向以挑剔著称的Apple公司创始人steve Jobs和Google公司创始人Larry Page都对其产品设计赞赏有加。他在报告演示了该产品的语音识别、人机对话、机器学习等功能，并介绍了其专利技术的理论原理。这个报告带来的启示是，软件理论并非只能是抽象、遥远的，它可以“管用”，甚至可以“很酷”。

 16日，来自清华大学、中科院软件所、华东师范大学的5位博士生报告了他们在软件理论领域的最新研究成果。

经过专家组40分钟的关门评议，我院孙家广院士的博士生孔辉所做“混成系统安全性验证的壁垒证明方法改进”获得最佳研究奖。

本次“清华软件日”活动由顾明教授、软件理论讲席教授Jean-Pierre Jouannaud筹备和主持。来自软件学院、计算机系、交叉信息研究院、中科院软件所、北京大学、国防科技大学、华东师范大学等单位的近百位师生参加了这次论坛。

本届“清华软件日”是继2011年百年校庆、十年院庆之际首创“清华软件日”之后，我院软件理论学科再次举办的重要国际学术交流活动，体现了软件理论研究“重在基础，强在应用，与时俱进”的特色。论坛提供的“高水平对话”平台对我院软件理论学科建设探索将起到积极的促进作用。