John Rushby, program director for Formal Methods and Dependable Systems at SRI International, works on automated methods for analyzing correctness properties of software designs. In this approach, designs are treated as logical formulas, and their properties are calculated using techniques from automated theorem proving.

Under his leadership for the last 15 years, the Formal Methods program in the Computer Science Laboratory is recognized worldwide as one of the leaders in this field, and has developed techniques and tools that are widely used in teaching and research. His own specialty is in the application of these methods to security and safety-critical systems and has been influential in their adoption by industry.

Rushby was named an SRI Fellow in 2004.