4月24日,应计算机科学国家重点实验室邀请,英国牛津大学Luke Ong教授到海洋之神8590vip软件研究所进行学术交流,并作了题为Automatic Verification of Message-Passing Concurrency的学术报告,报告会由林惠民研究员主持。
报告介绍了Luke Ong教授及其团队关于并发编程语言Erlang安全性验证的基础理论的研究成果。Erlang是最先于1980年代由爱立信计算机科学实验室提出的适用于电信等领域的大规模并发软件系统开发的高级编程语言。Luke Ong教授提出了新的一类可用于描述Erlang并发程序中通讯与并发执行等特征的形式化并发模型,新的模型涵盖了学界已有的异步函数调用计算模型,并能适用很大一类Erlang并发程序。
报告中,针对此新模型,Luke Ong教授阐述了解决其相应的安全性验证问题的算法,并确定了该问题的计算复杂度。此外,Luke Ong教授还介绍了其主持在研的Sorter项目,该项目旨在建立一套能直接为Erlang并发程序提供安全性验证的软件工具。
Luke Ong教授精彩的报告引起了大家广泛的兴趣,报告结束后,与会人员踊跃提问交流,Luke Ong教授就相关问题给予了回答。
Luke Ong现为英国牛津大学计算机科学教授、计算机科学系的研究生主任、以及墨顿学院理事会成员。他的主要研究领域为计算语义及逻辑。他在该领域的l-演算、类理论、并发理论、线性逻辑和计算证明理论等分支均有建树,尤其是引领了博弈语义分支的发展。