SRI’s pioneering methods of applying mathematical logic for rigorous reasoning about the correctness of computer software culminated in two important tools: the Hierarchical Development Methodology (HDM) formulated at SRI in the 1970s, and the Prototype Verification System (PVS) in the 1980s. Because of the need for the inviolability of critical national security software, development of HDM was sponsored by the National Security Agency. SRI funded development of PVS.
PVS is one of the world’s most widely used software creation programs. PVS includes an extremely expressive specification language and a high-performance mechanical theorem prover. It provides rigorous assurance of correctness for mission-critical software systems.
