SRI International

SRI International (formerly Stanford Research Institute) is an independent nonprofit research organization founded in 1946 and headquartered in Menlo Park, California. It is one of the most consequential research institutes in the history of computing, having produced inventions and foundational research that shaped entire fields.

SRI's contributions to formal methods and verification are central to the PVS story. The Prototype Verification System was developed at SRI's Computer Science Laboratory by Sam Owre, Natarajan Shankar, and John Rushby beginning in the early 1990s. PVS remains one of the most influential verification systems in aerospace and security applications, and its development at SRI established the institute as a center of formal methods research.

Beyond formal verification, SRI's innovations include the computer mouse (developed by Douglas Engelbart in the 1960s), the Shakey robot (one of the first mobile robots with planning capabilities), and the development of the natural language processing technology that became Apple's Siri. The institute has also produced foundational work in packet switching (the ARPANET), ultrasound, and materials science.

The connection between SRI and the NASA formal verification community is particularly strong. SRI researchers have collaborated extensively with NASA Langley Research Center on the verification of aerospace systems, including the Space Shuttle and aircraft collision avoidance algorithms. This collaboration has produced some of the largest applied formal verification libraries in existence.