Infrastructure for Development of Secure, Reliable Software

The Verification and Automated Reasoning research group at Cornell University has been building an infrastructure, comprising human expertise and computational resources, for the development of secure, reliable software for critical military applications. Such software includes distributed real-time embedded software systems, which are inherently complex and difficult to understand and specify. The infrastructure includes both efficient means of constructing the software and mathematically rigorous means of ensuring that the software will be secure and correct by construction.