Formal Program Verification
Heather K. Harton, Murali Sitaraman, Joan Krone · Wiley Encyclopedia of Computer Science and Engineering · 2008
Abstract Using formal program verification, it is possible to prove mathematically and mechanically that software behaves correctly as specified. For verification to scale up to software built from components, components must have formal specifications and the verification process must be modular. Unlike testing that can only reveal the presence of errors, formal varification can guarantee correctness.