资源介绍
这是一本学术会议论文集，汇集了第18届NASA形式化方法国际研讨会（NFM 2026）的精华成果，于2026年5月5日至7日在美国加利福尼亚州洛杉矶举行，由NASA喷气推进实验室（JPL）和南加利福尼亚大学（USC）联合组织举办，并被收录在施普林格旗下久负盛名的《计算机科学讲义》（Lecture Notes in Computer Science，LNCS）系列中，卷号为16622。本届研讨会的三位主编分别是来自南加州大学的Jyotirmoy Deshmukh教授，以及两位供职于NASA喷气推进实验室、加州理工学院的资深研究员Klaus Havelund和Alessandro Pinto，他们共同把控了论文集的学术方向和质量。NASA形式化方法研讨会自2009年起每年举办一届，此前先后在NASA旗下的多个研究中心轮换举办，包括兰利研究中心、艾姆斯研究中心、喷气推进实验室以及约翰逊航天中心，足见其在美国航空航天领域的深厚根基与广泛影响。本届会议共收到60篇投稿，经过67人程序委员会中至少三位成员的单盲评审以及10位领域主席的监督讨论，最终有25篇论文脱颖而出被收录其中，其中23篇为完整的研究论文，2篇为探讨新思路的短论文。除了常规论文之外，会议还邀请了六位学术界和工业界的重量级嘉宾发表主旨演讲，包括来自Harmonic公司的Tudor Achim、斯坦福大学的Clark Barrett教授、康奈尔大学的Hadas Kress-Gazit教授、亚马逊云科技的Rahul Kumar与Leonardo de Moura，以及NASA兰利研究中心的César Muñoz，其中两位嘉宾的论文也被收录在论文集中。论文所覆盖的研究主题相当广泛，既有自然语言需求的形式化、契约规约、定理证明与重写逻辑、概率模型检测等经典形式化方法领域，也包括近年来备受关注的前沿方向，比如静态分析、运行时验证、自动机学习、AI系统的形式化验证、AI辅助的形式化验证，以及大语言模型在形式化方法中的应用。这些技术被灵活运用于机器人、无人机、航空电子系统、信息物理系统乃至量子计算等高保障领域，反映了形式化方法在安全攸关系统中日益重要的地位。对于从事软件验证、形式化方法、嵌入式系统、航空航天软件工程、机器人与自主系统等方向的研究者和工程师而言，这本论文集提供了一个难得的窗口，可以一窥该领域最前沿的研究进展和实践经验，同时也是研究生和高年级本科生了解形式化方法如何应用于真实复杂工业场景的优秀参考读物。整本书由施普林格自然出版集团出版，ISBN为978-3-032-28079-4，具有较高的学术收藏价值。