Dr. John Rushby

A British legendary computer scientist in the field of formal methods and verification, he moved to the United States where he works for SRI International in Menlo Park California. He developed the Prototype Verification System, 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. Prior to joining SRI, he taught and did research for Manchester University in Manchester, England and later Newcastle University in Newcastle upon Tyne in North-East England. Born and brought up in London, England, he 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. From 1974 to 1975, he was a lecturer in the Computer Science Department at Manchester University and from 1979 to 1982 he was a research associate in the Department of Computing Science at the Newcastle University. In 1983 he 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 develops mechanized formal verification systems (the latest is called "PVS"), and applies them to problems in computer security, hardware design, and safety-critical and fault-tolerant systems. PVS is being 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 is 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. He was the recipient of 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 has authored or co-authored numerous publications, the latest of which is, ?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. He 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-present). He is the author of the section on formal methods for the FAA Digital Systems Validation Handbook (the guidelines for aircraft certification).