English Name: Gerard J. Holzmann

主要研究对象：软件可靠性、形式化方法与程序验证

         Gerard J. Holzmann 出生于荷兰阿姆斯特丹，后在美国长期从事软件可靠性与形式化方法研究与工程实践，具有“荷裔美国”背景。他早期在代尔夫特理工大学完成工程师学位与博士训练，研究主题与并发/多处理系统的协调问题相关；职业上，他在贝尔实验室计算科学研究中心工作多年，之后于 2003 年加入美国航空航天局喷气推进实验室，参与并推动建立“可靠软件实验室”，并在该机构承担软件可靠性相关的研发与工程把关工作。

         他的研究领域集中在软件可靠性与安全、形式化验证、逻辑模型检测、并发与分布式系统、静态源代码分析、代码评审与软件工程工具等方向；这些关键词在 CORE Academy 的成员页上被明确列为其主要研究兴趣，同时也给出他在加州理工学院计算机科学授课、以及在加州以研究合同形式开展工作的经历。

         在学术与工程贡献方面，他最具代表性的成果是开发并长期维护SPIN 模型检测器：该工具面向并发与分布式软件/协议的正确性验证，成为形式化验证领域被广泛使用的工具之一，并推动了“模型检测从理论走向工程实践”的一类典型路线。此后他在喷气推进实验室的工作重心更偏向高可靠软件的工程落地，包括将形式化方法、静态分析与严格代码评审流程用于航天任务软件质量控制；其公开简历中也记录了他在喷气推进实验室围绕任务软件的代码审查、编码规范与稳健性开展工作。

         除 SPIN 外，他还持续推动面向“大规模代码库”的静态分析与交互式代码检查工具实践（例如以研究与工程工具形式出现的相关工作），并提出过面向安全关键代码的工程化规则（如“十条规则”一类的编码与可靠性约束），强调用可执行的规范与可复核的流程降低缺陷风险。总体来看，他的贡献类型更像是把形式化方法、验证技术与工程流程结合起来：既有工具与方法层面的长期产出，也有在高可靠场景中推动其可用性与可落地性的系统实践。

Homepage(s): https://spinroot.com/gerard/ 

Core Academy Profile: https://coreacad.org/Member.aspx?ProId=151