• 团队成员：包括来自普林斯顿大学的 Andrew W. Appel 等、康奈尔大学的 David Bindel 等、密歇根大学的 Jean-Baptiste Jeannin 等及其他相关人员，还有来自不同机构的博士后、博士生和研究科学家等。
• 研究内容：采取分层方法对数值软件的正确性和准确性进行基础验证，即关于程序（不仅是算法）的形式化机器检查证明，除指令集架构规范外无其他假设，在各层构建、改进和使用适当工具，包括在实数中证明离散算法、证明浮点算法如何近似实数算法、推理浮点算法的 C 程序实现以及在 Coq 中连接所有证明等。
• 初始研究项目及结果：有cbench_vst/sqrt（牛顿法求平方根）、VerifiedLeapfrog（常微分方程的验证数值方法）、VCFloat2（Coq 中的浮点误差分析）、Parallel Dot Product（验证简单共享内存任务并行的正确性）、Stationary Iterative Methods（具有形式验证误差界的迭代方法）等。
• 参考文献：包含多篇相关研究论文，如关于混合精度算术的确定性和概率性舍入误差分析、浮点统计模型的方差感知舍入不确定性分析等。
• 资金支持：各项目部分得到国家科学基金会多项 grants 支持，如 2219757 给普林斯顿大学、2219758 给康奈尔大学、2219997 给密歇根大学，还有美国能源部计算科学研究生奖学金以及桑迪亚国家实验室的合作资助等。