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

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

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

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 formalmethods to verify the safety, security, and dependability oflarge-scale software systems. Foundational approaches (to formalmethods) emphasize expressiveness and generality, but they have notbeen successfully scaled to large-scale systems. Lightweightapproaches emphasize automation and scalability, but they are lesseffective on low-level programs and on providing explicit proofwitness. The PIs are developing new high-level and low-levellightweight methods and adapting them into various foundationalverification systems. More specifically, at the high level, the PIsare developing lightweight dependent-type systems andseparation-logic shape analysis, and connecting current methods such asconventional type systems, slicing analysis, and flow analysis; at thelow level, the PIs are designing specialized provers and decisionprocedures to verify low-level programs and to support certifiedlinking of heterogeneous components. If successful, this research willdramatically improve the scalability of foundational verificationsystems and provide new powerful technologies for building trustworthysoftware systems. Combining lightweight and foundational approachesalso provides a common thread that will pull different verificationcommunities together and unify them into a single framework

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