2011年10月17日,清华软件理论论坛在FIT楼1-315举行。论坛特别邀请了图灵奖获得者、美国卡耐基梅隆大学Edmund Clarke教授和研究类型论著名学者、英国伦敦大学罗朝晖教授,中国科学院院士、计算机程序形式化验证方面的专家林惠民院士,以及数位嵌入式系统研发领域的航天502所的专家。数十位博士和硕士研究生参加了该论坛。论坛由软件学院举办,孙家广院士主持。
Clarke教授就他们在软件形式化方法方面取得的最新理论成果以及在工业界的应用做了报告。Clarke教授提出基于抽象解释的理论用于化简复杂的工业模型,从而达到验证的目的。随后,罗朝晖教授做了有关类型论的报告,用通俗易懂的语言阐述了什么是类型论以及类型论在交互式定理证明工具中应用。最后,工业界的专家就他们在嵌入式系统开发和验证方面使用的方法和关心的问题给大家做了报告。

会后,大家就软件形式化理论如何在工业界推广和使用深入地交换了意见,工业界的专家们表示对形式化方法有着非常浓厚的兴趣,并希望以后加强合作与交流。