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.
