John Rushby | Academic Influence

John Rushby's AcademicInfluence.com Rankings

John Rushby

Computer Science

#2296

World Rank

#2393

Historical Rank

#1028

USA Rank

Database

#3701

World Rank

#3853

Historical Rank

#644

USA Rank

computer-science Degrees

Download Badge

Computer Science

John Rushby's Degrees

PhD Computer Science Stanford University
Masters Computer Science Stanford University

Similar Degrees You Can Earn

Why Is John Rushby Influential?

(Suggest an Edit or Addition)

According to Wikipedia, John Rushby is a British computer scientist now based in the United States and working for SRI International. He previously taught and did research for Manchester University and later Newcastle University.

(See a Problem?)

John Rushby's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

PVS: A Prototype Verification System (1992) (1784)
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS (1995) (673)
Design and verification of secure systems (1981) (503)
Noninterference, Transitivity, and Channel-Control Security Policies 1 (2005) (341)
A Tutorial Introduction to PVS (1998) (294)
Using model checking to help discover mode confusions and other automation surprises (2002) (254)
An Overview of SAL (2000) (219)
Critical system properties: survey and taxonomy (1994) (188)
Bus Architectures for Safety-Critical Embedded Systems (2001) (176)
Subtypes for Specifications: Predicate Subtyping in PVS (1998) (175)
An operational semantics for Stateflow (2004) (173)
A Comparison of Bus Architectures for Safety-Critical Embedded Systems (2003) (167)
An Invitation to Formal Methods (1996) (161)
Formal Methods and their Role in the Certification of Critical Systems (1997) (151)
Formal verification of algorithms for critical systems (1991) (148)
A Distributed Secure System (1983) (137)
Generating efficient test sets with a model checker (2004) (127)
Formal Methods and the Certification of Critical Systems (2004) (122)
Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1999) (122)
Proof of separability: A verification technique for a class of a security kernels (1982) (114)
Runtime Certification (2008) (89)
A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model (1993) (87)
PVS: An Experience Report (1998) (86)
The MILS component integration approach to secure information sharing (2008) (85)
The PVS Specification Language (1993) (83)
Model checking a fault-tolerant startup algorithm: from design exploration to exhaustive fault simulation (2004) (83)
User guide for the pvs specification and verification system (beta release) (1991) (81)
New challenges in certification for aircraft software (2011) (80)
Byzantine Agreement with Authentication : Observations andApplications in Tolerating Hybrid and Link Faults (1995) (72)
A Trusted Computing Base for Embedded Systems (1984) (71)
A Separation Kernel Formal Security Policy in PVS (2004) (70)
Pvs: Combining Speciication, Proof Checking, and Model Checking ? 1 Combining Theorem Proving and Typechecking (1996) (66)
Quality Measures and Assurance for AI Software1 (1988) (66)
Modular Certification (2002) (65)
Models and Mechanized Methods that Integrate Human Factors into Automation Design (2000) (65)
An Overview of Formal Verification for the Time-Triggered Architecture (2002) (63)
A Less Elementary Tutorial for the PVS Specification and Verification System (1996) (63)
A formally verified algorithm for interactive consistency under a hybrid fault model (1993) (61)
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model (1993) (60)
The ICS Decision Procedures for Embedded Deduction (2004) (59)
PVS Language Reference Version 2 . 4 • November 2001 (1998) (58)
Reasoning about the Reliability of Diverse Two-Channel Systems in Which One Channel Is "Possibly Perfect" (2012) (55)
A formally verified algorithm for clock synchronization under a hybrid fault model (1994) (55)
Formalism in Safety Cases (2010) (55)
An automated method to detect potential mode confusions (1999) (55)
Invisible formal methods for embedded control systems (2003) (54)
Analyzing Cockpit Interfaces Using Formal Methods (2001) (54)
A Tutorial on Using PVS for Hardware Verification (1994) (53)
The Interpretation and Evaluation of Assurance Cases (2015) (51)
Formally verified Byzantine agreement in presence of link faults (2002) (51)
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification (2000) (50)
Just-in-Time Certification (2007) (50)
Model-Based Reconfiguration: Toward an Integration with Diagnosis (1991) (50)
Safety envelope for security (2014) (49)
Theorem Proving for Verification (2000) (49)
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving (1999) (48)
Integration in PVS: Tables, Types, and Model Checking (1997) (47)
Evaluating, Testing, and Animating PVS Specications (2001) (46)
Sal 2 (2004) (45)
Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model (1994) (43)
Harnessing Disruptive Innovation in Formal Verification (2006) (43)
An Introduction to Formal Specification and Verification using EHDM (1991) (43)
Software Verification and System Assurance (2009) (40)
Low-Overhead Time-Triggered Group Membership (1997) (40)
Automated Test Generation and Verified Software (2005) (39)
Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems (1992) (38)
Disappearing formal methods* (2000) (37)
A case-study in component-based mechanical verification of fault-tolerant programs (1999) (35)
Formal Verification of the Interactive Convergence Clock Synchronization Algorithm using EHDM (1989) (34)
Formal Verification of a Fault Tolerant Clock Synchronization Algorithm (1989) (34)
Security Requirements Specifications : How and What ? Extended (2001) (34)
Modeling the Human in Human Factors (2001) (33)
A Safety-Case Approach For Certifying Adaptive Systems (2009) (33)
Logic and Epistemology in Safety Cases (2013) (32)
Toward a multi-method approach to formalizing human-automation interaction and human-human communications (2011) (31)
Acceptance of Formal Methods : Lessons from Hardware Design (1996) (31)
Formal Modeling and Analysis for Interactive Hybrid Systems (2011) (30)
The Versatile Synchronous Observer (2012) (29)
Separation and Integration in MILS (The MILS Constitution) (2008) (28)
Tutorial: Automated Formal Methods with PVS, SAL, and Yices (2006) (27)
Automated Deduction and Formal Methods (1996) (26)
An Evidential Tool Bus (2005) (24)
TTA and PALS: Formally verified design patterns for distributed cyber-physical systems (2011) (24)
Model Checking Simpson's Four-Slot Fully Asynchronous Communication Mechanism (2002) (24)
The Ontological Argument in PVS (2013) (24)
Quality Measures and Assurance for AI (Artificial Intelligence) Software (1988) (23)
Evaluation of an expert system for fault detection, isolation, and recovery in the manned maneuvering unit (1990) (22)
Formal Verification of McMillan's Compositional Assume-Guarantee Rule (2001) (21)
Considerations in Assuring Safety of Increasingly Autonomous Systems [STUB] (2018) (21)
The Bell and La Padula Security Model (1986) (21)
Using PVS to Prove Some Theorems Of David Parnas (1993) (21)
Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision (2011) (21)
Avionics Architectures: Mechanisms, and Assurance (1999) (21)
Understanding and Evaluating Assurance Cases (2015) (20)
Example of a Complementary Use of Model Checking and Human Performance Simulation (2014) (20)
Mechanized Support for Assurance Case Argumentation (2013) (19)
Distributed Secure Systems: Then and Now (2007) (18)
Specification, Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS (1997) (17)
Assurance 2.0: A Manifesto (2020) (17)
Formal Verification of Transmission Window Timing for the Time-Triggered Architecture (2001) (17)
The enhanced HDM system for specification and verification (1985) (17)
Formal verification of AI software (1989) (16)
A FAULT-MASKING AND TRANSIENT-RECOVERY MODEL FOR DIGITAL FLIGHT-CONTROL SYSTEMS (1993) (16)
Mechanized Formal Methods: Where Next? (1999) (16)
Structural Embeddings: Mechanization with Method (1999) (16)
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned (1993) (16)
Model Checking and Other Ways of Automating Formal Methods (1995) (15)
Reconfiguration and transient recovery in state machine architectures (1996) (15)
Trustworthy Self-Integrating Systems (2016) (15)
Systematic formal verification of interpreters (1997) (14)
Formal Specification and Verification for Critical Systems: Tools, Achievements, and Prospects (1991) (14)
On the Interpretation of Assurance Case Arguments (2015) (13)
Composing Safe Systems (2011) (13)
Formal methods and their role in digital systems validation for airborne systems (1995) (13)
Example of a Complementary Use of Model Checking and Agent-Based Simulation (2013) (13)
Mechanized Formal Methods: Progress and Prospects (1996) (12)
Mechanizing Formal Methods: Opportunities and Challenges (1995) (12)
Automated Formal Methods Enter the Mainstream (2007) (12)
Model-Centered Assurance for Autonomous Systems (2020) (11)
Calculating with requirements (1997) (11)
Dependable Computing for Critical Applications 7 (1999) (10)
SAL Tutorial: Analyzing the Fault-Tolerant Algorithm OM(1) (2004) (9)
From Refutation to Verification (2000) (9)
Evaluating the Assessment of Software Fault-Freeness (2014) (8)
Integrating Verification Components ⋆ (2005) (8)
Validation and Testing of Knowledge-Based Systems - How bad can it get? (1991) (8)
Design and Veriication of Secure Systems (1981) (8)
Assurance and Assurance Cases (2017) (8)
For Safety-Critical Embedded Systems ? (2001) (7)
A Mechanically Assisted Examination of Begging the Question in Anselm's Ontological Argument (2018) (6)
Formal Methods and Critical Systems In the Real World (2006) (6)
The Future of Formal Methods in Industry (1995) (6)
Formal Verification of an Oral Messages Algorithm for Interactive Consistency (2003) (6)
Formal methods for dependable real-time systems (1993) (6)
What Use is Verified Software? (2007) (6)
How Do We Certify For The Unexpected (2008) (6)
Design Choices In Specification Languages And Verification Systems (1991) (6)
A Tutorial on Using Pvs for Hardware Veriication ? Pvs Stands for \prototype Veriication System." It Consists of a Speciication Language Integrated with Support Tools and a Theorem Prover. Pvs Tries to Pro- ? (1995) (5)
Subtypes for specifications (1997) (5)
Security Requirements Specifications: How and What? Extended Abstract (2001) (5)
Formal Verification of Marzullo's Sensor Fusion Interval (2002) (5)
The Indefeasibility Criterion for Assurance Cases (2020) (5)
Modeling the Human in Human Factors Extended Abstract (2001) (5)
The Security Model of Enhanced HDM (2007) (5)
Ubiquitous abstraction: a new approach for mechanized formal verification (1998) (4)
Reports From Working Groups (1990) (4)
Mechanized Analysis Of a Formalization of Anselm ’ s Ontological Argument by Eder and Ramharter (2016) (4)
Industrial Practice (1996) (4)
Formal Verification and Automated Testing for Diagnostic and Monitoring Systems (2008) (3)
Systematic Formal Verication for Fault-Tolerant (1999) (3)
Expanded Version of a Paper from the Sixth Working Conference on Dependable Computing for Critical Applications, Systematic Formal Veriication for Fault-tolerant Time-triggered Algorithms (1997) (3)
From formal verification to silicon compilation (1991) (3)
On the (f)utility of untrusted data sanitization (2011) (3)
Formally Verified Hardware Encapsulation Mechanism for Security, Integrity, and Safety (2002) (3)
Formal Verification of Hybrid Byzantine Agreement Under Link Faults (2001) (3)
PVS Embeddings of Propositional and Quantified Modal Logic (2022) (3)
Mechanized analysis of Anselm’s modal ontological argument (2020) (3)
Embedded Deduction With ICS (2003) (3)
Software Verification and System Assurance (Invited Paper) (2009) (2)
LR(k) sparse-parsers and their optimisation (1977) (2)
A Formal Model for MILS Integration (2008) (2)
Integrating Verification Components : The Interface is the Message ? (2004) (2)
A Mechanically Assisted Examination of Vacuity and Question Begging in Anselm's Ontological Argument (2022) (2)
PARTITIONING IN AVIONICS: REQUIREMENTS, MECHANISMS, AND ASSURANCE. (2000) (1)
Assurance 2.0 (2020) (1)
AFM ’ 08 : Third Workshop on Automated Formal Methods 14 July 2008 Princeton , New Jersey (2008) (1)
Model-Based Reconfiguration: wit iag sis* (1991) (1)
The PVS Verification System and PC/DC (1994) (1)
Security , Safety , and Partitioning ? (1)
Inferring and Conveying Intentionality: Beyond Numerical Rewards to Logical Intentions (2022) (1)
The future of industrial formal methods (1995) (1)
Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23-27 November 2009 (2009) (1)
Algorithms for Fault Tolerant Distributed Systems (1989) (1)
From DSS to MILS - (Extended Abstract) (2011) (1)
Critical System Properties : Survey and Taxonomy 1 (1994) (1)
Automated Integration of Potentially Hazardous Open Systems (2017) (1)
A Scalable, Reconfigurable, and Dependable Time-Triggered Architecture (2003) (1)
An Application of the MILS Approach To Secure Information Sharing (2021) (1)
Subtypes for Speciications ? (1997) (1)
Algorithms for fault-tolerant distributed systems. Final technical report, February 1985-February 1988 (1989) (0)
[12] Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Some lessons learned. In J. C. P. Woodcock and P. G. Larsen, editors, (1993) (0)
Preliminary Formal Analysis of TTA Startup (2004) (0)
Combining System Properties: A Cautionary Example and Formal Examination (2005) (0)
Limits in Dependability (Panel) (1993) (0)
Compositional Abstraction and Refinement for Aspects (CARA) (2004) (0)
The Formal Veri cation of an Algorithmfor Interactive Consistency under a Hybrid FaultModel (2009) (0)
Structural Embeddings: Mechanization with Method Submitted to Fm99 for Consideration in the Foundations and Methodology Stream, Languages and Tools Mini-track (1999) (0)
Controlling Smart Technology (2022) (0)
Calculating with Requirements* (Extended Abstract) (1997) (0)
Test Suite Evaluation and Generation (2005) (0)
Systematic Formal Veri cation of Interpreters (1997) (0)
Systematic Formal Veri cation for Fault-TolerantTime-Triggered Algorithms (2009) (0)
Enhancing the utility of formal methods (1996) (0)
Biographies: Classic Paper (2007) (0)
Formal Analysis for Embedded Real-Time Systems (2006) (0)
A verified model of fault-tolerance (1990) (0)
Goal-Based Certification for Medical Devices (2005) (0)
Hybrid Systems - And Everything Else (2006) (0)
A Formal Methods Workbench for Critical Systems (2000) (0)
Proceedings of the second workshop on Automated formal methods (2007) (0)
Bayesian Network Models for Pattern and Plan Recognition (2000) (0)
Figure 3: Microprocessor Speciication Bolic Model Checking for Sequential Circuit Veriication. Ieee Transactions on 5 Conclusions and Future Work 4.2 Abstracting the Microprocessor Design 4.1 Proving the Lemmas Using Model-checking (0)
Figure 3: Microprocessor Speciication Bolic Model Checking for Sequential Circuit Veriication. Ieee Transactions on 5 Conclusions and Future Work 4.2 Abstracting the Microprocessor Design 4.1 Proving the Lemmas Using Model-checking (0)
Networks are Systems A Discussion Paper (2007) (0)
Enhan ing PVS to Support Evaluating , Testing , and Animating PVS Spe i (2007) (0)
Survivable Loosely Coupled Architectures (2003) (0)
Specifying real-time systems with interval logic (1988) (0)
Engineering for Artificial Intelligence Software (1990) (0)
Assessing Confidence with Assurance 2.0 (2022) (0)
Disappearing Formal Methods* Abstract (2000) (0)
Using Model Checking and Simula- Tion to Detect a Safety Violation in a Control System Speciication. Submitted for Publication (1998) (0)
Technology and Consciousness (2022) (0)
From Reviews to Analysis : Challenge and Opportunity Converge (2003) (0)
What FM can offer DFCS design (1990) (0)

This paper list is powered by the following services:

Other Resources About John Rushby

en.wikipedia.org

What Schools Are Affiliated With John Rushby?

John Rushby is affiliated with the following schools: