TC: Large: Collaborative Research: Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software

TC：大型：协作研究：结合基础和轻量级形式方法来构建可证明可靠的软件

• 批准号: 0910660
• 负责人: John Morrisett
• 金额: $ 57万
• 依托单位: Harvard University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-07-01 至 2013-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0910660&HistoricalAwards=false
• 关键词: TC; Large; Collaborative; Research; Combining

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5). This research focuses on combining foundational and lightweight formal methods to verify the safety, security, and dependability of large-scale software systems. Foundational approaches (to formal methods) emphasize expressiveness and generality, but they have not been successfully scaled to large-scale systems. Lightweight approaches emphasize automation and scalability, but they are less effective on low-level programs and on providing explicit proof witness. The PIs are developing new high-level and low-level lightweight methods and adapting them into various foundational verification systems. More specifically, at the high level, the PIs are developing lightweight dependent-type systems and separation-logic shape analysis, and connecting current methods such as conventional type systems, slicing analysis, and flow analysis; at the low level, the PIs are designing specialized provers and decision procedures to verify low-level programs and to support certified linking of heterogeneous components. If successful, this research will dramatically improve the scalability of foundational verification systems and provide new powerful technologies for building trustworthy software systems. Combining lightweight and foundational approaches also provides a common thread that will pull different verification communities together and unify them into a single framework.

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。本研究的重点是结合基础和轻量级的形式化方法来验证大规模软件系统的安全性、可靠性和可靠性。基础方法（形式方法）强调表达性和通用性，但它们还没有成功地扩展到大规模系统。轻量级方法强调自动化和可伸缩性，但它们在低级程序和提供显式证明证据方面不太有效。PI正在开发新的高级和低级轻量级方法，并将其应用于各种基础验证系统。更具体地说，在高层次上，PI正在开发轻量级的依赖类型系统和分离逻辑形状分析，并连接当前的方法，如传统的类型系统，切片分析和流分析;在低层次上，PI正在设计专门的证明器和决策过程，以验证低层次的程序，并支持异构组件的认证链接。如果成功，这项研究将大大提高基础验证系统的可扩展性，并为构建可信赖的软件系统提供新的强大技术。结合轻量级和基础方法还提供了一个共同的思路，将不同的验证社区聚集在一起，并将它们统一到一个框架中。