The End of Testing? The Promise of Verification-Driven Software Engineering

Abstract
Most of the effort of engineering goes into preventing and correcting bugs. Practicing engineers greatly value tools that move bug discovery earlier, from deployment to testing, or better yet from testing to compile-time type checks. Systems software verification is the application of machine-checked proofs to software engineering. It is the limiting case of eager bug discovery: once a program passes verification, it has no bugs except for those in the spec that describes its contract and its environment.

The primary impediment to replacing testing with software verification is cost: Historically, proofs were so fantastically expensive that you’d never even try until the program was empirically bug-free. Contemporary developments are driving these costs way down. The promise of verification-driven engineering is emerging into reality.

Biography
Jon Howell is a Principal Researcher in the VMware Research Group pursuing the applicability and deployment of verification as a practical engineering tool.