中国计算机学会形式化方法专委走进高校系列报告会于海南大学成功举办

2023年3月24号上午，由中国计算机学会形式化方法专委主办、海南大学承办的CCF形式化方法专委走进高校系列活动（海南大学）在海南大学计算机科学与技术学院504报告厅成功举行。本期报告会邀请了CCF形式化方法专委西南大学刘志明教授、国防科技大学计算机学院董威教授、西北工业大学董云卫教授、同济大学刘关俊教授等四位专家学者做学术报告。

报告会开始由海南大学计算机科学与技术学院副院长谢夏教授致欢迎词并介绍了报告会背景，对各位专家学者的到来表示热烈的欢迎和衷心的感谢。在本次报告会上，专家们围绕“程序智能合成、软件抽象、协同无人系统软件定义自动化、可信软件方法”做了精彩报告，并在问答环节就形式化方法领域的多个前沿学术问题、热点应用问题进行了深入的探讨，引起了广泛的共鸣。

董云卫教授的报告题目是“从Chat GPT 谈软件工程的未来——基于深度学习的程序合成技术”。主要介绍了以Chat GPT为代表的生成式神经元网络技术的快速发展和逐步成熟应用，对软件工程理论和技术的发展迎来巨大的机遇和前所未有的挑战。传统的软件开发技术将被替代，软件工程师的能力培养和工作角色也将发生巨大变革，基于深度学习的程序合成技术就是在这样的背景下发展起来的，它利用深度学习技术自动生成满足用户意图的目标程序。董教授的报告从Chat GPT的发展开始，介绍了生成神经元网络模型在软件开发过程中户意图理解、程序理解、模型训练、模型测试等角度的技术发展成果，总结了每一类方法的主要涉及思想并讨论当前程序合成技术还面临的一些技术挑战和研究热点，并对软件合成技术的发展趋势进行展望。

刘志明教授的报告题目是“软件系统与软件工程发展中的抽象”。主要内容是关于在软件系统与软件工程80余年的发展过程中，程序员和软件工程师从实践中发现提出了许多重要的抽象，这些抽象升级为理论研究，进而通过算法、语言、系统软件和设计模式实现。这些抽象概念、机制和模式是软件系统和软件工程发展与实践的重要的推动因素，是软件工程中最重要的研究和技术成果，也是计算机专业教育的核心内容。刘教授指出计算机科学技术与软件工程的本科教育应该为学生建立理解有关这些抽象的原理、理论、实现方法，并在实践课中练习系统地使用。

董威教授的报告题目是“面向无人系统协同的软件定义自动化方法”。人机物融合系统HCPS越来越受到广泛重视，其中面向具体任务和场景，自动、高效地生成满足要求的无人系统控制程序具有重要研究与应用价值，但也具有非常高的难度，尤其是对于需要协同的多无人系统更具有挑战性。董教授首先对人机物融合系统的发展进行了简要描述，然后对以程序综合与验证为基础的协同无人系统软件定义自动化工作进行了介绍。

刘关俊教授的报告题目是“并发系统模型与分析：由自动机模型到机器学习模型”。主要介绍了刘关俊教授团队在基于Petri网的模型检测上的一些研究工作。另外，深度强化学习近年来在无人系统领域得到越来越多的重视，这种由机器学习生成的系统控制模块在应对复杂的运行环境以及应对系统自身复杂的交互协同上抱有极大的期望，然而这种训练出的决策模型在可解释性、鲁棒性等诸多方面仍有很长的路要走，刘教授也介绍了一些在这方面的思考与相关研究。

此次CCF走进高校系列报告内容精彩纷呈，会议过程高潮迭起，让所有与会人员享受了一场学术盛宴。在报告会提问环节，在座的老师和同学们积极地提出自己在科学研究中所遇到的问题，专家们耐心并详细地作了回答，使大家受益匪浅。刘志明教授还为在场的同学们赠送了新书《数理逻辑引论：计算机科学与系统的天然基础》。最后，参加报告会的现场听众对四位特邀讲者表示由衷的欢迎与感谢，报告会在掌声中圆满结束。