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

点击翻译按钮获取中文摘要

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