Program Director, Formal Methods and Dependable Systems, Computer Science Laboratory
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.
Recent publications
-
The Versatile Synchronous Observer
The paper describes and illustrates these applications of synchronous observers.
-
Safety Envelope for Security
We present an approach for detecting sensor spoofing attacks on a cyber-physical system. Our approach consists of two steps. In the first step, we construct a safety envelope of the system. In the second step, we build an attack detector: a monitor that executes synchronously with the system and raises an alarm whenever the system state falls outside…
-
Logic and Epistemology in Safety Cases