| 2013 | SMC | Example of a Complementary Use of Model Checking and Agent-Based Simulation. | Gabriel Gelman, Karen M. Feigh, John M. Rushby |
| 2011 | EMSOFT | New challenges in certification for aircraft software. | John M. Rushby |
| 2011 | SMC | 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 |
| 2009 | SEFM | Software Verification and System Assurance. | John M. Rushby |
| 2008 | RV | Runtime Certification. | John M. Rushby |
| 2007 | ACSAC | Distributed Secure Systems: Then and Now. | Brian Randell, John M. Rushby |
| 2007 | ICECCS | Just-in-Time Certification. | John M. Rushby |
| 2007 | ICECCS | What Use is Verified Software? | John M. Rushby |
| 2006 | SEFM | Harnessing Disruptive Innovation in Formal Verification. | John M. Rushby |
| 2006 | SEFM | Tutorial: Automated Formal Methods with PVS, SAL, and Yices. | John M. Rushby |
| 2005 | ICFEM | An Evidential Tool Bus. | John M. Rushby |
| 2004 | CADE | The ICS Decision Procedures for Embedded Deduction. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar |
| 2004 | CAV | SAL 2. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
| 2004 | DSN | Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation. | Wilfried Steiner, John M. Rushby, Maria Sorea, Holger Pfeifer |
| 2004 | FASE | An Operational Semantics for Stateflow. | Grgoire Hamon, John M. Rushby |
| 2004 | SEFM | Generating Efficient Test Sets with a Model Checker. | Grgoire Hamon, Leonardo Mendona de Moura, John M. Rushby |
| 2002 | ICDCS | Formally Verified Byzantine Agreement in Presence of Link Faults. | Ulrich Schmid, Bettina Weiss, John M. Rushby |
| 2001 | EMSOFT | Bus Architectures for Safety-Critical Embedded Systems. | John M. Rushby |
| 2001 | SAFECOMP | Modeling the Human in Human Factors. | John M. Rushby |
| 2000 | CAV | Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. | John M. Rushby |
| 2000 | FORTE | From Refutation to Verification. | John M. Rushby |
| 1999 | FM | Structural Embeddings: Mechanization with Method. | Csar A. Muoz, John M. Rushby |
| 1999 | FM | Mechanized Formal Methods: Where Next? | John M. Rushby |
| 1998 | FM | PVS: An Experience Report. | Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert |
| 1998 | ICFEM | Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. | John M. Rushby |
| 1997 | ICFEM | Systematic Formal Verification of Interpreters. | David Cyrluk, John M. Rushby, Mandayam K. Srivas |
| 1997 | RE | Calculating with Requirements. | John M. Rushby |
| 1997 | TACAS | Integration in PVS: Tables, Types, and Model Checking. | Sam Owre, John M. Rushby, Natarajan Shankar |
| 1996 | CAV | PVS: Combining Specification, Proof Checking, and Model Checking. | Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
| 1996 | CAV | Automated Deduction and Formal Methods. | John M. Rushby |
| 1994 | PODC | A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model. | John M. Rushby |
| 1993 | CAV | The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. | Patrick Lincoln, John M. Rushby |
| 1993 | FM | Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. | Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke |
| 1992 | CADE | PVS: A Prototype Verification System. | Sam Owre, John M. Rushby, Natarajan Shankar |
| 1991 | AAAI | Model-Based Reconfiguration: Toward an Integration with Diagnosis. | Judith Crow, John M. Rushby |
| 1983 | SP | A Distributed Secure System. | John M. Rushby, Brian Randell |
| 1981 | SOSP | Design and Verification of Secure Systems. | John M. Rushby |