Design and Verification of Secure Systems. - John M. Rushby (SOSP, 1981)

Proof of separability: A verification technique for a class of a security kernels. - John M. Rushby (Symposium on Programming, 1982)

A Distributed Secure System. - John M. Rushby; Brian Randell (Computer, 1983)

Model-Based Reconfiguration: Toward an Integration with Diagnosis. - Judith Crow; John M. Rushby (AAAI, 1991)

From formal verification to silicon compilation. - Jeffrey Joyce; Erwin Liu; John M. Rushby; Natarajan Shankar; Roberto Suaya; Friedrich W. von Henke (Compcon, 1991)

Design Choices in Specification Languages and Verification Systems. - John M. Rushby (TPHOLs, 1991)

PVS: A Prototype Verification System. - Sam Owre; John M. Rushby; Natarajan Shankar (CADE, 1992)

Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. - John M. Rushby (FTRTFT, 1992)

The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. - Patrick Lincoln; John M. Rushby (CAV, 1993)

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. - Sam Owre; John M. Rushby; Natarajan Shankar; Friedrich W. von Henke (FME, 1993)

Limits in Dependability (Panel). - Jean-Claude Laprie; Gérard Le Lann; Michele Morganti; John M. Rushby (FTCS, 1993)

A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model. - Patrick Lincoln; John M. Rushby (FTCS, 1993)

Using PVS to Prove Some Theorems Of David Parnas. - John M. Rushby; Mandayam K. Srivas (HUG, 1993)

Formal Verification of Algorithms for Critical Systems. - John M. Rushby; Friedrich W. von Henke (IEEE Trans. Software Eng., 1993)

The PVS Verification System and PC/DC. - John M. Rushby; Jens Ulrik Skakkebæk (FTRTFT, 1994)

A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model. - John M. Rushby (PODC, 1994)

A Tutorial on Using PVS for Hardware Verification. - Sam Owre; John M. Rushby; Natarajan Shankar; Mandayam K. Srivas (TPCD, 1994)

The Future of Formal Methods in Industry. - Anthony Hall; David Lorge Parnas; Nico Plat; John M. Rushby; Chris T. Sennett (ZUM, 1995)

Mechanizing Formal Methods: Opportunities and Challenges. - John M. Rushby (ZUM, 1995)

Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. - Sam Owre; John M. Rushby; Natarajan Shankar; Friedrich W. von Henke (IEEE Trans. Software Eng., 1995)

PVS: Combining Specification, Proof Checking, and Model Checking. - Sam Owre; S. Rajan; John M. Rushby; Natarajan Shankar; Mandayam K. Srivas (CAV, 1996)

Automated Deduction and Formal Methods. - John M. Rushby (CAV, 1996)

Mechanized Formal Methods: Progress and Prospects. - John M. Rushby (FSTTCS, 1996)

Reconfiguration and Transient Recovery in State Machine Architectures. - John M. Rushby (FTCS, 1996)

An Invitation to Formal Methods. - Jonathan P. Bowen; Ricky W. Butler; David L. Dill; Robert L. Glass; David Gries; Anthony Hall; Michael G. Hinchey; C. Michael Holloway; Daniel Jackson 001; Cliff B. Jones; Michael J. Lutz; David Lorge Parnas; et al. (Computer, 1996)

Enhancing the Utility of Formal Methods. - John M. Rushby (ACM Comput. Surv., 1996)

Subtypes for Specifications. - John M. Rushby (ESEC / SIGSOFT FSE, 1997)

Systematic Formal Verification of Interpreters. - David Cyrluk; John M. Rushby; Mandayam K. Srivas (ICFEM, 1997)

Calculating with Requirements. - John M. Rushby (RE, 1997)

Integration in PVS: Tables, Types, and Model Checking. - Sam Owre; John M. Rushby; Natarajan Shankar (TACAS, 1997)

Low-Overhead Time-Triggered Group Membership. - Shmuel Katz; Patrick Lincoln; John M. Rushby (WDAG, 1997)

PVS: An Experience Report. - Sam Owre; John M. Rushby; Natarajan Shankar; David W. J. Stringer-Calvert (FM-Trends, 1998)

Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. - John M. Rushby (ICFEM, 1998)

Subtypes for Specifications: Predicate Subtyping in PVS. - John M. Rushby; Sam Owre; Natarajan Shankar (IEEE Trans. Software Eng., 1998)

Structural Embeddings: Mechanization with Method. - César A. Muñoz; John M. Rushby (World Congress on Formal Methods, 1999)

Mechanized Formal Methods: Where Next? - John M. Rushby (World Congress on Formal Methods, 1999)

Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving. - John M. Rushby (SPIN, 1999)

A case-study in component-based mechanical verification of fault-tolerant programs. - Sandeep S. Kulkarni; John M. Rushby; Natarajan Shankar (WSS, 1999)

Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. - John M. Rushby (IEEE Trans. Software Eng., 1999)

Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. - John M. Rushby (CAV, 2000)

From Refutation to Verification. - John M. Rushby (FORTE, 2000)

Theorem Proving for Verification. - John M. Rushby (MOVEP, 2000)

Analyzing Cockpit Interfaces Using Formal Methods. - John M. Rushby (FM-Everywhere@FORTE/PSTV, 2000)

Bus Architectures for Safety-Critical Embedded Systems. - John M. Rushby (EMSOFT, 2001)

Modeling the Human in Human Factors. - John M. Rushby (SAFECOMP, 2001)

An Overview of Formal Verification for the Time-Triggered Architecture. - John M. Rushby (FTRTFT, 2002)

Formally Verified Byzantine Agreement in Presence of Link Faults. - Ulrich Schmid 001; Bettina Weiss; John M. Rushby (ICDCS, 2002)

Invisible formal methods for embedded control systems. - Ashish Tiwari 001; Natarajan Shankar; John M. Rushby (Proc. IEEE, 2003)

The ICS Decision Procedures for Embedded Deduction. - Leonardo Mendonça de Moura; Sam Owre; Harald Rueß; John M. Rushby; Natarajan Shankar (IJCAR, 2004)

SAL 2. - Leonardo Mendonça de Moura; Sam Owre; Harald Rueß; John M. Rushby; Natarajan Shankar; Maria Sorea; Ashish Tiwari 001 (CAV, 2004)

Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation. - Wilfried Steiner; John M. Rushby; Maria Sorea; Holger Pfeifer (DSN, 2004)

Generating Efficient Test Sets with a Model Checker. - Grégoire Hamon; Leonardo Mendonça de Moura; John M. Rushby (SEFM, 2004)

An Evidential Tool Bus. - John M. Rushby (ICFEM, 2005)

Automated Test Generation and Verified Software. - John M. Rushby (VSTTE, 2005)

Hybrid Systems - And Everything Else. - John M. Rushby (HSCC, 2006)

Harnessing Disruptive Innovation in Formal Verification. - John M. Rushby (SEFM, 2006)

Tutorial: Automated Formal Methods with PVS, SAL, and Yices. - John M. Rushby (SEFM, 2006)

PVS. - Bart Jacobs 001; John M. Rushby (The Seventeen Provers of the World, 2006)

Distributed Secure Systems: Then and Now. - Brian Randell; John M. Rushby (ACSAC, 2007)

Just-in-Time Certification. - John M. Rushby (ICECCS, 2007)

What Use is Verified Software? - John M. Rushby (ICECCS, 2007)

Automated Formal Methods Enter the Mainstream. - John M. Rushby (J. Univers. Comput. Sci., 2007)

An operational semantics for Stateflow. - Grégoire Hamon; John M. Rushby (Int. J. Softw. Tools Technol. Transf., 2007)

Runtime Certification. - John M. Rushby (RV, 2008)

Software Verification and System Assurance. - John M. Rushby (SEFM, 2009)

Formalism in Safety Cases. - John M. Rushby (SSS, 2010)

From DSS to MILS - (Extended Abstract). - John M. Rushby (Dependable and Historic Computing, 2011)

Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision. - Mark-Oliver Stehr; Carolyn L. Talcott; John M. Rushby; Patrick Lincoln; Minyoung Kim 002; Steven Cheung; Andy Poggio (Formal Modeling: Actors, Open Systems, Biological Systems, 2011)

New challenges in certification for aircraft software. - John M. Rushby (EMSOFT, 2011)

Toward a multi-method approach to formalizing human-automation interaction and human-human communications. - Ellen J. Bass; Matthew L. Bolton; Karen M. Feigh; Dennis Griffith; Elsa L. Gunter; William Mansky; John M. Rushby (SMC, 2011)

Formal Modeling and Analysis for Interactive Hybrid Systems. - Ellen J. Bass; Karen M. Feigh; Elsa L. Gunter; John M. Rushby (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

The Versatile Synchronous Observer. - John M. Rushby (SBMF, 2012)

Example of a Complementary Use of Model Checking and Agent-Based Simulation. - Gabriel Gelman; Karen M. Feigh; John M. Rushby (SMC, 2013)

Safety envelope for security. - Ashish Tiwari 001; Bruno Dutertre; Dejan Jovanovic; Thomas de Candia; Patrick Lincoln; John M. Rushby; Dorsa Sadigh; Sanjit A. Seshia (HiCoNS, 2014)

Example of a Complementary Use of Model Checking and Human Performance Simulation. - Gabriel Gelman; Karen M. Feigh; John M. Rushby (IEEE Trans. Hum. Mach. Syst., 2014)