John Rushby

Developer of the Prototype Verification System (PVS), a major impetus for the development of computer science, Rushby is a British computer scientist legendary in the field of formal methods and verification. He has worked for SRI International in Menlo Park, California. PVS is a specification language integrated with support tools and an automated theorem prover. Automated theorem proving (ATP), also known as automated deduction, is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

Born and brought up in London, England, Rushby attended Dartford Grammar School. He studied at Newcastle University in the United Kingdom, earning his B.Sc. degree in Computer Science in 1971 and his Ph.D. in 1977. Prior to joining SRI, he taught and did research at Manchester University in Manchester, England and later at Newcastle University in Newcastle upon Tyne in North-East England.

From 1974 to 1975, he served as a lecturer in the Computer Science Department at Manchester University, and from 1979 to 1982 he served as a research associate in the Department of Computing Science at Newcastle University. In 1983 Rushby joined SRI International as a Computer Scientist, then as Senior Computer Scientist. He then became a Program Manager and, from 1986 to 1990, the Acting Program Director of the Computer Science Laboratory (CSL).

He then became Program Director for Formal Methods and Dependable Systems, where his group developed mechanized formal verification systems (the latest of which is called "PVS"), and applied them to problems in computer security, hardware design, and safety-critical and fault-tolerant systems. PVS was used in industrial projects applying formal methods and automated verification to aerospace problems in collaboration with Honeywell, JPL, Lockheed Martin, NASA Langley, and Rockwell-Collins. His main area of interest has been the design and assurance of "critical systems", including properties such as security and safety, mechanisms such as kernelization and fault tolerance, and formal methods for assurance.

Rushby received the 2011 Harlan D. Mills Award from the IEEE Computer Society "For practical and fundamental contributions to Software & Hardware Reliability with seminal contributions to computer security, fault tolerance, and formal methods." In 2012 he was awarded, along with Sam Owre and Natarajan Shankar, the CAV Award "for developing PVS (Prototype Verification System) which, due to its early emphasis on integrated decision procedures and user friendliness, significantly accelerated the application of proof assistants to real-world verification problems."

He authored or co-authored numerous publications, the latest of which was "Example of a Complementary Use of Model Checking and Human Performance Simulation" with Gabriel Gelman and Karen M. Feigh, IEEE Transactions on Human-Machine Systems, Oct 2014, pp. 576–590. Rushby has served on the program committees for many conferences and as Associate Editor for the journals Communications of the ACM (1986–96) and Formal Aspects of Computing (1995–2014). He has also authored the section on formal methods for the FAA Digital Systems Validation Handbook, the guidelines for aircraft certification.