由华东师范大学承办的第十三届自动化验证与分析国际学术会议（13th International Symposium on Automated Technology for Verification and Analysis）于2015年10月11日至15日在上海召开。本次大会由我校何积丰院士任大会主席，德国Saarland大学Bernd Finkbeiner教授，中科院软件所张立军教授，华东师范大学蒲戈光教授任程序委员会共同主席。

图为大会主席何积丰院士与会

       本次大会有来自英国、法国、美国、丹麦等国际领域内顶级专家学者60余名，包括美国工程院院士 J Strother Moore教授、欧洲科学院院士Joost-Pieter Katoen教授、Ernst-Ruediger Olderog教授、Kim G. Larsen教授等，以及国内包括中国科学院、北京大学、上海交通大学、西安电子科技大学、华东师范大学等的专家学者40余名学者参加。会议分为了SMT，程序验证，概率系统，工具，测试用例及反例自动生成，验证，合成，和混合系统等七个部分，分别以大会报告、邀请报告、口头报告等多种交流方式进行。

图为会议现场

       受大会邀请，德克萨斯大学计算理论名誉主席J Strother Moore教授在会上做了专题报告，讲述通过Boyer-Moore定理以及实例证明将计算机硬软件建立成可在具体数据环境下运行的数据模型的可行性，以及ACL2如何交互使用ACL2去证实一些简单问题以及证明一些形式化定理。

图为J Strother Moore教授

       伦敦大学皇家工程学院Dino Distefano教授，一直是国际软件验证方面的专家，在会议上作了题为Moving fast with software verification的邀请报告，重点介绍了基于形式化验证技术下，对于Facebook软件开发周期静态分析工具的整合过程。

图为Dino Distefano教授

       亚琛工业大学Joost-Pieter Katoen教授，围绕程序建模与验证方向，报告探讨验证概率程序中有关循环、分析参数化方案和终止程序概率方面的问题，研究了Markov模型的算法性能和一些相关应用，以及近期的概率模型检测的发展。

图为Joost-Pieter Katoen教授报告

       会上，奥登堡大学混合系统研究组教授Martin Fränzle探讨了物联网的安全性和可靠性以及这方面的一些自动化分析技术的覆盖性和局限性。

图为Martin Fränzle教授

       本次大会重点在计算机验证方法，包括模型检查、形式化方法等领域进行交流，探讨计算机理论发展前沿。我校软件工程学科近些年取得了长足的发展，并取得了一系列引人瞩目的成果，本次会议由我校承办与召开，并由我校计算机科学与bet体育365官网正规院长何积丰院士担任大会主席，印证与提升了我校在该领域的国际影响力。截止到当前，本会议已经先后在世界十几个城市举办，会议旨在促进国内形式化方法领域的发展，同时为来自世界各地的科学家搭建桥梁，共享研究成果，促进学术交流，探讨及建立合作。

图为参会成员在华东师范大学合影