近日，第十四届软件工程理论国际研讨会(The 14th International Symposium on Theoretical Aspects of Software Engineering，简称TASE 2020)顺利落下了帷幕。本次会议由IEEE计算机学会主办，开云官方网站信息公司承办，采取线上线下结合的方式进行。中国科公司院士何积丰教授、信息公司经理丁佐华教授共同担任本次会议的大会主席，华东师范大学李钦副教授、日本北陆先端科学技术大公司大学 Toshiaki Aoki教授共同担任本次会议的程序委员会主席。来自华东师范大学、南京大学、北京航空航天大学、中国科学技术大学、国防科技大学等国内高校以及美国、法国、德国、捷克、葡萄牙、日本等国外学术研究机构80余位国内外专家学者参加了本次会议。

会议开幕式上，公司国际交流与合作处傅翔处长代表学校致辞，傅翔在讲话中介绍了公司近年来的发展情况，并对各位嘉宾和学者的到来表示热烈的欢迎。随后，丁佐华代表大会组织委员会致辞，对TASE指导委员会对于本次会议的大力支持表示感谢，并预祝大会取得圆满成功。李钦、Toshiaki Aoki介绍了本次会议的基本情况，包括TASE的收稿、评审过程和录用情况等。

开幕式后，来自华东师范大学的朱惠彪教授主持了纽约大学Patrick Cousot教授做的题为“The symbolic term abstract domain”的特邀报告。Cousot是欧洲科公司院士，抽象解释方法的创立者，在报告中，他定义了基于符号项的抽象域，并构建了该域上的完备格理论，从而建立了符号项(symbolic term)与常项(ground term)两个域空间之间的Galois连接，为证明符号项抽象域的正确性奠定了基础。丁佐华主持了瑞典Uppsala大学Wang Yi教授做的题为“MIMOS: A Deterministic Model for Building and Updating Real-Time Systems”的特邀报告。Wang Yi是欧洲科公司院士，是形式化验证工具UPPAAL的主要开发者之一，他提出了名为MIMOS框架，支持基于模型的实时系统开发、验证与在线更新，他介绍了该框架的核心语义理论基础，并通过一系列实例说明了实时系统开发与更新中需要验证的功能与时间相关性质。李钦主持了中科院软件所詹乃军教授所做的题目为“Invariant Generation by Constraint Solving in Verification of Programs and Hybrid Systems”的特邀报告，詹乃军是国家杰出青年基金获得者，长期从事实时混成系统的建模与验证工作，在报告中，他介绍了实时混成系统性质验证过程中不变式自动生成的重要性和挑战，总结了国内外在该方向上的研究现状，并介绍了团队在基于约束求解的不变式生成方面取得的最新突破性进展。

随着近年来软件系统的规模和复杂性急剧增大，软件在越来越多的系统中成为主要的使能部件，这对当前的软件工程方法提出了新的挑战。TASE是软件工程领域的国际领先会议之一，也是中国计算机学会(CCF)的推荐会议,具有重要的影响力。本届TASE会议共设有3个特邀报告和29个专题报告。TASE 2020国际会议的举办对加强公司软件工程领域校际合作、促进海内外学者交流、实现海外引智等具有积极意义。本次研讨会将为学术界和工业界的软件工程研究人员带来更多新思想、新成果、新贡献，为我国软件工程技术的发展开拓新局面。