TRUSTEES OF PRINCETON UNIVERSITY, THE
Grant: $500,000 - National Science Foundation - Jul. 1, 2009
No votes have been cast for this award yet
Join the conversation: Post a comment about this award
Award Description: 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.
Project Description: As defined in the project abstract.
Jobs Summary: NA (Total jobs reported: 0)
Project Status: Less Than 50% Completed
This award's data was last updated on Jul. 1, 2009. Help expand these official descriptions using the wiki below.
No comments have been added for this project.