iProve: A Scalable Approach to Consumer-Verifiable Software Guarantees

Formally proving complex program properties is still considered impractical for systems with over a million lines of code (MLOC). We present iProve, an approach that enables the generation and verification of proofs for interesting program properties in large Java systems. Desired properties are proven in iProve as a combination of two proofs: one of a complex property applied to a very tiny part of the code—a nucleus—and a proof of a simple property applied to the rest of the code—the body. We use iProve to prove properties such as communication security, deadlock immunity, data privacy, and resource usage bounds in Java programs with millions of LOC. iProve scales well, requires no access to source code, and allows nuclei to be reused with an unlimited number of systems and to be written in verification-friendly languages.

Published in:
Proceedings of the Intl. Conference on Dependable Systems and Networks (DSN)
Presented at:
Intl. Conference on Dependable Systems and Networks (DSN), Chicago, IL, June 2010
Ieee Service Center, 445 Hoes Lane, Po Box 1331, Piscataway, Nj 08855-1331 Usa

 Record created 2010-03-15, last modified 2018-03-17

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)