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

该奖项是根据2009年《美国复苏和再投资法案》(Public Law 111-5)资助的。本研究致力于结合基础和轻量级形式方法来验证大型软件系统的安全性、安全性和可靠性。基本方法(形式化方法)强调表现力和概括性，但它们还没有成功地扩展到大规模系统。轻量级方法强调自动化和可伸缩性，但它们对低级程序和提供明确的证据是不有效的。PIS正在开发新的高级别和低级别轻量级方法，并将其应用于各种基础验证系统。更具体地说，在高层，PI正在开发轻量级依赖类型系统和分离逻辑形状分析，并连接现有方法，如常规类型系统、切片分析和流分析；在较低级别，PI正在设计专门的证明器和决策程序，以验证低级别程序并支持异类组件的认证链接。如果成功，这项研究将极大地提高基础验证系统的可扩展性，并为构建可信软件系统提供新的强大技术。将轻量级方法和基础方法相结合还提供了一条公共线索，将不同的验证社区结合在一起，并将它们统一到单个框架中

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