SRI International Computer Science Laboratory

Recent Papers by John Rushby

Fast Links: 2024 | 2023 | 2022 | 2021 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1992 | 1991 | 1989 | 1988 | 1986 | 1985 | 1984 | 1983 | 1982 | 1981 | 1977 | 1974 Problems viewing these papers?

Our web server has been ugraded and you can now reference these pages securely using https instead of the former http; this should happen automatically if you come in via an https link.

My ORCID is 0000-0002-6604-9953

And my arXiv public author identifier is http://arxiv.org/a/rushby_j_1

And my Erdos Number is 3.

Links to videos and to slides.

I was honored to receive the IEEE Harlan D Mills Award for 2011 (picture).

And Sam Owre, Shankar and I received the Computer-Aided Verification (CAV) Award for 2012 (picture)
and also the Skolem Award in 2021 for the most influential paper from CADE-11 that was held in 1992.

According to my Google Scholar profile, my H-index is 60.

Information about Assurance 2.0

Photos from some meetings and retirements

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

2024

• "Models are Central to AI Assurance by Robin Bloomfield and John Rushby. Presented at ASSURE24 workshop, part of ISSRE, Tsukuba, Japan, October 2024
• Assurance 2.0 in a Nutshell (PDF) by Robin Bloomfield and John Rushby. CSL Technical Note October 2024. We also have a separate web page for Assurance 2.0
• Enabling Theory-based Continuous Assurance: A Coherent Approach with Semantics and Automated Synthesis, by Srivatsan Varadarajan and others including John Rushby. Presented at SASSUR Workshop, Sept 2024, published in SafeComp Workshops, Springer LNCS 14989. pp 173--187
• Confidence in Assurance 2.0 Cases by Robin Bloomfield and John Rushby. Also available as arXiv 2409.10665.
  Expanded version of a paper from The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part I. Springer LNCS 14780, pp. 1--23, Sept 2024
• Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP by Anitha Murugesan and several others, including John Rushby, to appear in special issue of TPLP but already available at arXiv 2408.11699. Extended version of GDE23
• Assurance of AI Systems From a Dependability Perspective by Robin Bloomfield and John Rushby, Technical Report SRI-CSL-2024-02, July 2024; also available as arXiv 2407.13948.
• Defeaters and Eliminative Argumentation in Assurance 2.0 by Robin Bloomfield, Kate Netkachova, and John Rushby, Technical Report SRI-CSL-2024-01, May 2024; also available as arXiv 2405.15800. See also major update to Assessing Confidence in Assurance 2.0

• CLARISSA: Foundations, Tools & Automation for Assurance Cases by Srivatsan Varadarajan and several others, including John Rushby, presented at DASC 23, Barcelona Spain, October 2023
• Semantic Analysis of Assurance Cases Using s(CASP) by Anitha Murugesan and several others, including John Rushby, presented at ICLP 2023 Workshop on Goal-Directed Execution of Answer Set Programs (GDE), London, July 2023.
• On Computational Mechanisms for Shared Intentionality and Speculation on Rationality and Consciousness by John Rushby, SRI-CSL Technical Report, May 2023. Also available as arXiv 2306.13657

• Controlling Smart Technology: A Brief Review of Some Ethical Challenges by John Murray, John Rushby, and Daniel Sanchez. The International Review of Information Ethics, vol 33, no 1, 2022. Based on our report Technology and Consciousness
• Talk: Models and their Validation and their Role in Perception--and in Safe Autonomous Vehicles, Presented at a virtual meeting of IFIP WG 10.4 on 11 May 2022
• Assessing Confidence in Assurance 2.0 by Robin Bloomfield and John Rushby, Technical Report SRI-CSL-2022-02, May 2022 and also available as arXiv 2205.04522, both revised May 2024

• Mechanized Analysis of Anselm's Modal Ontological Argument by John Rushby. International Journal for Philosophy of Religion, April 2021. First published online 4 August 2020. Minor update available as arXiv:2205.08628
• Assurance 2.0: A Manifesto by Robin Bloomfield and John Rushby, keynote presentation at 29th Safety-Critical Systems Symposium (SSS'21), February 2021. Draft available as arXiv 2004.10474

• I was a participant in The 2020 Expert Survey on Formal Methods presented at FMICS 2020 and published in Springer LNCS 12327.
• Model-Centered Assurance For Autonomous Systems by Susmit Jha, John Rushby, and N. Shankar. Presented at SafeComp, September 2020. Published in Springer LNCS 12234.
• The Indefeasibility Criterion for Assurance Cases by John Rushby. Springer, July 2020. Postproceedings of a Shonan Workshop held in November 2016; the paper was updated in 2019 and published in 2020 so I'm filing it here.
• Assurance 2.0: A Manifesto by Robin Bloomfield and John Rushby, on arXiv, now published in 29th Safety-Critical Systems Symposium (SSS'21)
• A Mechanically Assisted Examination of Vacuity and Question Begging in Anselm's Ontological Argument by John Rushby. Appears as Chapter 13 in the book "Beyond Faith and Rationality: Essays on Logic, Religion and Philosophy" published by Springer. This updates the version published in IfCoLog 5(7), 2018 by showing that all versions of the argument considered entail variants that are vulnerable to Gaunilo's refutation. Updated version also available as arXiv:2205.14071

• Inferring and Conveying Intentionality: Beyond Numerical Rewards to Logical Intentions by Susmit Jha and John Rushby. Presented at TOCAIS 2019: Towards Conscious AI Systems Symposium (part of AAAI SSS-19), Stanford CA, March 25-27, 2019 and also available as arXiv 2207.05058
• Technology and Consciousness by John Rushby and Daniel Sanchez. This is a report on a series of workshops held in 2017; the report was written in 2018 and released in 2019, so I'm filing it under 2019. The 30-page introduction is a good overview of consciousness topics. Also available as arXiv 2209.03956

• A Mechanically Assisted Examination of Begging the Question in Anselm's Ontological Argument by John Rushby. Journal of Applied Logics, Vol. 5 No. 7, pp. 1473--1496, October 2018 (journal version of the conference paper from 2017).
  Note: this paper is now obsolete and is replaced by this extended version.
• Considerations in Assuring Safety of Increasingly Autonomous Systems by Erin E. Alves, Devesh Bhatt, Brendan Hall, Kevin Driscoll, Anitha Murugesan (all of Honeywell), and John Rushby. This is a NASA project report (local copy).

• PVS Embeddings of Propositional and Quantified Modal Logic by John Rushby. SRI-CSL Technical Report, November 2017, minor revision May 2022. Also available as arXiv:2205.06391.
• Automated Integration of Potentially Hazardous Open Systems by John Rushby. Invited paper, presented at Workshop on Open Systems Dependability (WOSD) 2017, Keio University, Japan, October 2017.
• A Mechanically Assisted Examination of Begging the Question in Anselm's Ontological Argument by John Rushby. Presented at 2nd World Congress on Logic and Religion, Warsaw, June 2017.
  Note: this paper is now obsolete and is replaced by this extended version.

• Assurance and Assurance Cases by John Rushby. Slightly updated from Marktoberdorf Summer School Lectures, 2016, pp. 207-236. Published by IOS Press October 2017, ed. A. Pretschner, D. Peled and T. Hutzelmann
• Mechanized Analysis of a Formalization of Anselm's Ontological Argument by Eder and Ramharter by John Rushby. CSL Technical Note, January 2016.
• Trustworthy Self-Integrating Systems by John Rushby. Presented at the 12th International Conference on Distributed Computing and Internet Technology (ICDCIT), Bhubaneswar, India, January 2016; published in Springer LNCS Vol. 9581, pp. 19--29

• On the Interpretation of Assurance Case Arguments by John Rushby. Presented at the Second International Workshop on Argument for Agreement and Assurance (AAA 2015), Keio University, Kanagawa, Japan, November 2015 Proceedings published as Springer LNAI vol. 10091.
• The Interpretation and Evaluation of Assurance Cases by John Rushby. Technical Report SRI-CSL-15-01, July 2105

• Example of a Complementary Use of Model Checking and Human Performance Simulation by Gabriel Gelman, Karen M. Feigh, and John Rushby. Appears in IEEE Transactions on Human-Machine Systems, Oct 2014, pp. 576-590.
• Safety Envelope For Security by Ashish Tiwari, Bruno Dutertre, Dejan Jovanovic, Thomas de Candia, Patrick D Lincoln, John Rushby, Dorsa Sadigh, and Sanjit Seshia. Presented at the 3rd International Conference On High Confidence Networked Systems.
• Evaluating the Assessment of Software Fault-Freeness by Bev Littlewood, John Rushby, and Lorenzo Strigini. Presented at workshop on Assessing the Efficacy of Standards for Safety Critical Software (AESSCS 2014), Newcastle upon Tyne UK, 13 May 2014
• The Versatile Synchronous Observer by John Rushby. Presented at Specification, Algebra, and Software, A Festschrift Symposium in Honor of Kokichi Futatsugi (SAS 2014), Kanazawa Japan, April 2014. Published in Springer LNCS vol. 8373.

• Mechanized Support For Assurance Case Argumentation by John Rushby. Presented at The 1st International Workshop on Argument for Agreement and Assurance (AAA 2013), Kanagawa Japan, October 2013. Proceedings published as Springer LNAI vol. 8417
• Logic and Epistemology in Safety Cases by John Rushby. Invited paper, presented at Computer Safety, Reliability, and Security: SafeComp 32, Toulouse, France, September 2013, appears in Springer LNCS Vol. 8153.
• The Ontological Argument in PVS by John Rushby. Invited paper presented at the CAV Workshop Fun With Formal Methods, St. Petersburg, Russia, 13 July 2013.

• Reasoning about the Reliability Of Diverse Two-Channel Systems In which One Channel is "Possibly Perfect" by Bev Littlewood (City University, UK) and John Rushby. IEEE Transactions on Software Engineering, Vol. 38, No. 5, September/October 2012, Pages~1178--1194.
• New Challenges In Certification For Aircraft Software by John Rushby. Substantially revised version of a paper presented at the Ninth ACM International Conference On Embedded Software (EMSOFT).

• Composing Safe Systems by John Rushby. Invited paper, presented at the 8th International Symposium on Formal Aspects of Component Software (FACS'11), Oslo, Norway, September 14-16, 2011
• TTA and PALS: Formally Verified Design Patterns for Distributed Cyber-Physical Systems by Wilfried Steiner and John Rushby, presented at the 30th IEEE/AIAA Digital Avionics Systems Conference (DASC), Seattle WA, October 2011
• Formal Modeling and Analysis for Interactive Hybrid Systems by Ellen J. Bass, Karen M. Feigh, Elsa Gunter, and John Rushby. Presented at 4th International Workshop on Formal Methods for Interactive Systems: FMIS 2011, Limerick, Ireland, 21 June 2011
• From DSS to MILS (extended abstract) by John Rushby. Presented at "Randell's Tales: a Festschrift recognizing the contributions of Brian Randell", C.B. Jones and J.L Lloyd (Eds.), Springer LNCS 6875, pp. 53--57, August 2011.
• Formal Methods for Test Case Generation by John Rushby, Leonardo De Moura, and Gregoire Hamon. US Patent 7865339, issued 4 January 2011 (filed 12 July 2004).

• Formalism in Safety Cases by John Rushby. Apppears in Making Systems Safer: Proceedings of the Eighteenth Safety-Critical Systems Symposium, Bristol UK, February 2010. Published by Springer.
• Reasoning about the Reliability Of Diverse Two-Channel Systems In which One Channel is "Possibly Perfect" by Bev Littlewood (City University, UK) and John Rushby. Technical Report SRI-CSL-09-02, updated January 2010 and December 2010

• Software Verification and System Assurance, by John Rushby. Invited paper, presented at SEFM09: Software Engineering and Formal Methods, Hanoi, Vietnam, November 2009
• A Safety-Case Approach For Certifying Adaptive Systems , by John Rushby. AIAA Infotech@Aerospace Conference, Seattle WA, April 2009
• An Application of the MILS Approach to Secure Information Sharing, by Rance DeLong (LynuxWorks, San Jose CA), David Hanz (SRI) and John Rushby (SRI). Unpublished, November 2009

• The MILS Component Integration Approach to Secure Information Sharing , by Carolyn Boettcher, Raytheon, El Segundo CA; Rance DeLong, LynuxWorks, San Jose CA; John Rushby, SRI International, Menlo Park CA; and Wilmar Sifre, AFRL/RITB, Rome NY. Presented at the 27th IEEE/AIAA Digital Avionics Systems Conference (DASC), St. Paul MN, October 2008.
• Formal Verification and Automated Testing for Diagnostic and Monitoring Systems , by Bruno Dutertre, Cesar Munoz, John Rushby, Radu Siminiceanu and Ashish Tiwari. Presented at AIAA Guidance, Navigation and Control Conference, Honolulu HI, August 2008
• Separation and Integration in MILS: The MILS Constitution , by John Rushby. SRI-CSL Technical Report February 2008.
• Runtime Certification, by John Rushby. Invited paper, presented at RV2008: Eighth Workshop on Runtime Verification, Budapest, Hungary, April 2008.

• Distributed Secure Systems: Then and Now, by Brian Randell and John Rushby. Presented as a "Classic Paper" at the 2007 Annual Computer Security Applications Conference (ACSAC 23), Miami FL.
• An Operational Semantics for Stateflow by Gregoire Hamon and John Rushby. International Journal on Software Tools for Technology Transfer (STTT), Volume 9, Numbers 5-6, October 2007; Special section FASE'04/05, Pages 447--456.
• Software for Dependable Systems: Sufficient Evidence? Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors, Committee on Certifiably Dependable Software Systems (of which I was a member), National Research Council. You can get a free PDF version of the report from the link above.
• Just-in-Time Certification, by John Rushby. Presented at the 12th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand
• What Use Is Verified Software?, by John Rushby. Invited paper, presented in a special session on the Verified Software Initiative at the 12th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand
• Automated Formal Methods Enter the Mainstream, by John Rushby. Communications of the Computer Society of India, Vol. 31, No. 2, May 2007, pp. 28-32. Formal Methods Special Theme Issue.

• Harnessing Disruptive Innovation in Formal Verification, by John Rushby. Invited paper, presented at the 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Pune, India, September 2006, © IEEE Computer Society.

• Integrating Verification Components, by Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and Natarajan Shankar. Invited position paper for Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, October 2005.
• Automated Test Generation And Verified Software by John Rushby. Invited position paper for Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, October 2005. Updated for LNCS volume due 2007.
• Automated Test Generation with SAL by Gregoire Hamon, Leonardo de Moura, and John Rushby. CSL Technical Note, January 2005.

• Generating Efficient Test Sets with a Model Checker by Gregoire Hamon, Leonardo de Moura, and John Rushby. Presented at SEFM '04, Beijing, China, September 2004.
• SAL Tutorial: Analyzing the Fault-Tolerant Algorithm OM(1) by John Rushby. CSL Technical Note, April 2004.
• The ICS Decision Procedures for Embedded Deduction by Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and N. Shankar. Presented at IJCAR 2004, Cork, Ireland. Appears in Springer Verlag LNCS 3097, pp. 218-222.
• SAL 2 by Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari. Presented at CAV 2004, Boston, MA. Appears in Springer Verlag LNCS 3114, pp. 496-500.
• Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation by Wilfried Steiner, John Rushby, Maria Sorea, and Holger Pfeifer. Presented at DSN '04, Florence, Italy, June 2004; proceedings published by IEEE Computer Society, pp. 189-198.
• An Operational Semantics for Stateflow by Gregoire Hamon and John Rushby. Presented at FASE '04, Barcelona, Spain, March 2004. Appears in Springer Verlag LNCS 2984, pp. 229-243.

2003

• The Needham-Schroeder Protocol in SAL by John Rushby. CSL Technical Note, October 2003.
• Embedded Deduction With ICS by Leonardo de Moura, Harald Ruess, John Rushby, and Natarajan Shankar. Presented at the National Security Agency's Third High Confidence Software and Systems Conference, Baltimore MD, April 2003.
• Invisible Formal Methods for Embedded Control Systems by Ashish Tiwari, John Rushby, and Natarajan Shankar. Proceedings of the IEEE, 91(1): 29-39, January 2003.

• Model Checking Simpson's Four-Slot Fully Asynchronous Communication Mechanism by John Rushby. CSL Technical Report, July 2002.
• An Overview of Formal Verification for the Time-Triggered Architecture by John Rushby. Presented at FTRTFT 2002, Oldenburg, Germany, September 2002. Appears in Springer Verlag LNCS 2469, pp. 83-105.
• Formally Verified Byzantine Agreement in Presence of Link Faults by Ulrich Schmid, Bettina Weiss, and John Rushby. ICDCS '02, Vienna, Austria, July 2002, pp. 608-616.
• Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises by John Rushby. In Reliability Engineering and System Safety Vol. 75, No. 2 (February 2002), pages 167-177.
• Formal Verification of Marzullo's Sensor Fusion Interval by John Rushby. CSL Technical Report, January 2002.

• A Comparison of Bus Architectures for Safety-Critical Embedded Systems by John Rushby. CSL Technical Report, September 2001.
• Bus architectures for safety-critical embedded systems by John Rushby. In Tom Henzinger and Christoph Kirsch, editors, EMSOFT 2001: Proceedings of the First Workshop on Embedded Software, Volume 2211 of Lecture Notes in Computer Science, pages 306-323, Lake Tahoe, CA, October 2001. Springer-Verlag.
• Modular Certification by John Rushby. CSL Technical Report, September 2001.
• Modeling the Human in Human Factors (extended abstract) by John Rushby. Invited paper in Udo Voges, editor, SafeComp 2001: Proceedings of the 20th International Conference on Computer Safety, Reliability, and Security, Volume 2187 of Lecture Notes in Computer pp Science, pages 86-91, Budapest, Hungary, September 2001. Springer-Verlag.
• Formal Verification of McMillan's Compositional Assume-Guarantee Rule by John Rushby. CSL Technical Report, September 2001.
• Evaluating, Testing, and Animating PVS Specifications by Judy Crow, Sam Owre, John Rushby, N. Shankar, and Dave Stringer-Calvert. CSL Technical Report, March 2001.
• Security requirements specifications: How and what? Invited paper presented at Symposium on Requirements Engineering for Information Security (SREIS), Indianapolis, IN, March 2001. Proceedings available on CD-ROM from http://www.cerias.purdue.edu.
• Analyzing Cockpit Interfaces Using Formal Methods Invited paper presented at FM-Elsewhere, Pisa, Italy, October 2000. Published in Proceedings of FM-Elsewhere, volume 43 of Electronic Notes in Theoretical Computer Science, Elsevier 2001.
• Formal Verification of Transmission Window Timing for the Time-Triggered Architecture by John Rushby. CSL Technical Report, March 2001.

• Disappearing Formal Methods by John Rushby. Invited paper presented at HASE: Fifth IEEE International Symposium on High Assurance Systems Engineering, 15-17 November, 2000, Albuquerque New Mexico
• From refutation to verification by John Rushby. Invited paper presented at Formal Description Techniques and Protocol Specification, Testing and Verification FORTE XIII/PSTV XX 2000, Pisa, Italy, October 2000. Chapman & Hall, UK.
• Models and mechanized methods that integrate human factors into automation design by Judith Crow, Denis Javaux, and John Rushby. In International Conference on Human-Computer Interaction in Aeronautics: HCI-Aero 2000, Toulouse, France, September 2000.
• Verification diagrams revisited: Disjunctive invariants for easy verification by John Rushby. In E. A. Emerson and A. P. Sistla, editors, Computer-Aided Verification, CAV '2000, volume 1855 of Lecture Notes in Computer Science, pages 508-520, Chicago, IL, July 2000. Springer-Verlag.
  
• Theorem proving for verification by John Rushby. In Franck Cassez, editor, Modelling and Verification of Parallel Processes: MoVEP 2k, Nantes, France, June 2000. Tutorial presented at MoVEP. Springer LNAI volume 2067.
  
• An overview of SAL by Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saïdi, N. Shankar, Eli Singerman, and Ashish Tiwari. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187-196, Hampton, VA, June 2000. NASA Langley Research Center. Proceedings available at http://techreports.larc.nasa.gov/ltrs/refer/2000/cp/NASA-2000-cp210100.refer.html

• Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms by John Rushby. IEEE Transactions on Software Engineering, Vol. 25, No. 5 (Sept.Oct. 1999), pp. 651-660.
• An Automated Method To Detect Potential Mode Confusions by John Rushby, Judy Crow (SRI), and Everett Palmer (NASA Ames). Presented at The 18th Digital Systems Avionics Conference (DASC), St Louis, October 1999.
• Structural Embeddings: Mechanization with Method by César Muñoz and John Rushby. In The World Congress on Formal Methods: FM 99, Toulouse, France, September 1999. Springer-Verlag Lecture Notes in Computer Science, Vol. 1708.
• Mechanized Formal Methods: Where Next? by John Rushby. Invited paper presented at The World Congress on Formal Methods: FM 99, Toulouse, France, September 1999. Springer-Verlag Lecture Notes in Computer Science, Vol. 1708.
• Partitioning in Avionics Architectures: Requirements, Mechanisms, and Assurance by John Rushby. NASA Contractor Report CR-1999-209347. Also issued by the FAA.
• Integrated Formal Verification: Using Model Checking With Automated Abstraction, Invariant Generation, and Theorem Proving, by John Rushby. Invited paper presented at 5th SPIN workshop (Part of the Federated Logic Conference, FLoC'99), Trento, Italy, July 1999. Appears in Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops, Springer Verlag Lecture Notes in Computer Science volume 1680.
• Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises by John Rushby. Presented at The 3rd Workshop on Human Error, Safety, and System Development (HESSD'99), Liege, Belgium, 7--8 June 1999 and appears in Reliability Engineering and System Safety, 75(2): 167-177, February 2002.
• A case study in component-based mechanical verification of fault-tolerant programs by Sandeep Kulkarni, John Rushby, and N. Shankar. In ICDCS Workshop on Self-Stabilizing Systems. IEEE Computer Society, June 1999.

• Ubiquitous Abstraction: A New Approach for Mechanized Formal Verification by John Rushby. Invited paper presented at the Second IEEE International Conference on Formal Engineering Methods (ICFEM '98), Brisbane, Australia, December 1998, pp.~176--178.
• PVS: An Experience Report by Sam Owre, John Rushby, N. Shankar, and David Stringer-Calvert. Appreas in Applied Formal Methods--FM-Trends 98, Dieter Hutter, Werner Stephan, Paolo Traverso, and Markus Ullman Eds., Springer Verlag Lecture Notes in Computer Science Vol. 1641, pp. 338--345, Boppard, Germany, October 1998
• Subtypes for Specifications: Predicate Subtypes in PVS by John Rushby Sam Owre, and N. Shankar. Appears in IEEE Transactions on Software Engineering, Vol. 24, No. 9 (Sept. 1998), pp. 709-720.

• Systematic Formal Verification of Interpreters by David Cyrluk, John Rushby, and Mandayam Srivas, presented at the First IEEE International Conference on Formal Engineering Methods (ICFEM '97), Hiroshima, Japan, November, 1997, pp 140-149.
• Subtypes for Specifications by John Rushby. Invited paper presented at the Fifth ACM Symposium on Foundations of Software Engineering and Sixth European Software Engineering Conference, Zurich, Switzerland, September 1997. Springer Verlag Lecture Notes in Computer Science Vol. 1301, pp. 4-19.
• Low-overhead Time-Triggered Group Membership by Shmuel Katz, Pat Lincoln, and John Rushby, presented at the 11th International Workshop on Distributed Algorithms (WDAG '97), Saarbrucken Germany, September 24-26, 1997. Springer-Verlag Lecture Notes in Computer Science Vol. 1320, pp. 155-169.
• Integration in PVS: Tables, Types, and Model Checking by Sam Owre, John Rushby, and Natarajan Shankar, presented at the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97), Enschede, The Netherlands, April 1997. Appears in volume 1217 of Lecture Notes in Computer Science, pages 366-383.
• Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms by John Rushby, presented at the Sixth Working Conference on Dependable Computing for Critical Applications, Garmisch-Partenkirchen, Germany, March, 1997. IEEE Computer Society Press, pp. 203-222.
• Calculating with Requirements by John Rushby. Invited paper presented at 3rd IEEE International Symposium on Requirements Engineering, Annapolis, MD, January, 1997, pp. 144-146.

• A Less Elementary Tutorial for the PVS Specification and Verification System by David Stringer-Calvert and John Rushby. CSL Technical Report CSL-95-10.
• Automated Deduction and Formal Methods by John Rushby. Invited paper presented to joint session of CAV and CADE '96. Appears in proceedings of CAV '96, Springer Verlag LNCS 1102, pp. 169-183, July 1996, New Brunswick, NJ.
• PVS: Combining Specification, Proof Checking, and Model Checking by S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. Presented at CAV '96, Springer Verlag LNCS 1102, pp. 411-414, July 1996, New Brunswick, NJ.
• Reconfiguration and Transient Recovery in State Machine Architectures by John Rushby. Presented at Fault Tolerant Computing Symposium (FTCS) 26, pp 6-15, Sendai, Japan, June 1996
• Acceptance of Formal Methods: Lessons from Hardware Design by David L. Dill and John Rushby, IEEE Computer April 1996 (Vol. 29, No. 4, pp. 23--24).
• Mechanized Formal Methods: Progress and Prospects by John Rushby. Invited paper presented at the 16th Conference on the Foundations of Software Technology and Theoretical Computer Science, Springer Verlag LNCS 1180, pp. 45--51, December 1996, Hyderabad, India.
• Analyzing Tabular and State-Transition Requirements Specifications in PVS by Sam Owre, John Rushby, and Natarajan Shankar. CSL Technical Report CSL-95-12

• Model Checking and Other Ways of Automating Formal Methods, by John Rushby. Position paper for panel on Model Checking for Concurrent Programs, presented at Software Quality Week, San Francisco, May/June 1995.
• Byzantine Agreement with Authentication: Observations and Applications in Tolerating Hybrid and Link Faults, by Li Gong, Patrick Lincoln, and John Rushby. Presented at Dependable Computing for Critical Applications--5, Champaign, IL, September 1995. IEEE Computer Society Press, pp. 139-157.
• Mechanizing Formal Methods: Opportunities and Challenges, by John Rushby. Preprint of an invited paper presented at the Z User's Meeting, Limerick, Ireland, September 1995
• Formal Methods and their Role in the Certification of Critical Systems by John Rushby. Technical Report CSL-95-1, March 1995. Also available as NASA Contractor Report 4673, August 1995, and issued as part of the FAA Digital Systems Validation Handbook (the guide for aircraft certification)
• A Tutorial Introduction to PVS by Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995
• Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS by Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke, IEEE Transactions on Software Engineering Vol. 21, No. 2 pp 107--125, February 1995

• A Tutorial on Using PVS for Hardware Verification by S. Owre and J. M. Rushby and N. Shankar and M. K. Srivas, presented at the 2nd International Conference on Theorem Provers in Circuit Design, September 1994, Springer Verlag LNCS 901, pp. 258--279
• A Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model by John Rushby, presented at PODC '94 (Los Angeles, August 94)
• Formal Verification of an Interactive Consistency Algorithm for the Draper FTP Architecture Under a Hybrid Fault Model" by Patrick Lincoln and John Rushby, from Compass '94 (Washington DC, June)
• Critical System Properties: Analysis and Taxonomy by John Rushby, published in Reliability Engineering and System Safety, Vol. 43, No. 2, pp. 189--219, 1994
• Model-Based Reconfiguration: Diagnosis and Recovery by Judith Crow and John Rushby. NASA Contractor Report 4596, May 1994

• Formal Methods and the Certification of Critical Systems by John Rushby. Technical Report SRI-CSL-93-7. Also issued under the title Formal Methods and Digital Systems Validation for Airborne Systems as NASA CR 4551.
• Formal Verification of Algorithms for Critical Systems by John Rushby and Friedrich von Henke, from IEEE Transactions on Software Engineering, vol. 19, no. 1, pp. 13-23, Jan 1993
• A Formally Verified Algorithm for Interactive Consistency under a Hybrid Fault Model by Patrick Lincoln and John Rushby, from Fault Tolerant Computing Symposium, FTCS 23, Toulouse, France, June, 1993
• Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model by Patrick Lincoln and John Rushby, in "Computer Aided Verification, CAV '93", Elounda, Greece, Jun-Jul, 1993.
• A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model by Patrick Lincoln and John Rushby. Technical Report CSL-93-02, March 1993. Also available as NASA Contractor Report 4527, July 1993
• Using PVS to Prove Some Theorems of David Parnas by John Rushby and Mandayam Srivas, from Proceedings of the 1993 International Workshop on the HOL Theorem Proving System and its Applications, Vancouver, Canada, Aug, 1993
• A Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems by John Rushby. Chapter 5 (pp. 237-257) in Jan Vytopil, ed., "Formal Techniques in Real-Time and Fault-Tolerant Systems", Kluwer International Series in Engineering and Computer Science, 1993.

• Noninterference, Transitivity, and Channel-Control Security Policies by John Rushby, SRI-CSL-92-02, December 1992
• PVS: A Prototype Verification System by S. Owre and J. M. Rushby and N. Shankar, from the 11th Conference on Automated Deduction, Deepak Kapur ed., Saratoga, NY, Jun, 1992
  Winner of the Skolem Award in 2021 for the most influential paper of CADE-11.
  
• Formal Methods for Dependable Real-Time Systems, by John Rushby, an invited paper presented at the International Symposium on Real-Time Embedded Processing for Space Applications, Les Saintes-Maries-de-la-Mer, France, November, 1992
• Formal Verification of an Oral Messages Algorithm for Interactive Consistency by John Rushby. Technical Report CSL-92-01, July 1992. Also available as NASA Contractor Report 189704, October 1992

• Model-Based Reconfiguration: Toward an Integration with Diagnosis by Judith Crow and John Rushby. Presented at AAAI-91, Anaheim, CA, July 1991
• From Formal Verification to Silicon Compilation by J. Joyce (Department of Computer Science, University of British Columbia), E. Liu, J. Rushby, N. Shankar, R. Suaya, and F. von Henke. from Proceedings of IEEE Compcon, San Francsico CA, February 1991, pp. 450-455
• Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems by John Rushby. Technical Report CSL-91-3, June 1991. Also available as NASA Contractor Report 4384
• An Introduction to Formal Specification and Verification Using EHDM by John Rushby, Friedrich von Henke, and Sam Owre. Technical Report CSL-91-2, February 1991.

• Kernels for Safety? by John Rushby, published in: T. Anderson, editor, Safe and Secure Computing Systems, chapter 13, pages 210--220. Blackwell Scientific Publications, 1989
• Formal Methods and Critical Systems in the Real World by John Rushby. Presented at Formal Methods for Trustworthy Computer Systems (FM89), Halifax, Nova Scotia, Canada, July 1989.
• Formal Verification of the Interactive Convergence Clock Synchronization Algorithm by John Rushby and Friedrich von Henke. Technical Report CSL-89-3R February 1989, Revised August 1991. Unrevised version also available as NASA Contractor Report 4239

• Validation and Testing of Knowledge-Based Systems: How Bad can it get? by John Rushby. Position Paper for AAAI-88 Workshop on Validation and Testing of Knowledge-Based Systems, reprinted in Uma G. Gupta, editor, Validating and Verifying Knowledge-Based Systems, pp. 76--82. IEEE Computer Society, Los Alamitos, CA, 1991
• Quality Measures and Assurance for AI Software by John Rushby. Technical Report CSL-88-7R, September 1988. Also available as NASA Contractor Report 4187

• The Bell and La Padula Security Model by John Rushby. Draft Technical Note, June 1986.

• Networks Are Systems by John Rushby. Proceedings of the Department of Defense Computer Security Center Invitational Workshop on Network Security, New Orleans, LA, March 1985. Reprinted in Marshall D. Abrams and Harold J. Podell, editors, Tutorial: Computer and Network Security, IEEE Computer Society Press, 1986, pp. 300--316.
• The Enhanced HDM System for Specification and Verification by Michael Melliar-Smith and John Rushby, presented at VerkShop III, Watsonville, CA, Feb 1985. Published as ACM Software Engineering Notes, Vol. 10, No. 41-43, Aug. 85

• A Trusted Computing Base for Embedded Systems by John Rushby. Proceedings 7th DoD/NBS Computer Security Conference, Gaithersburg, Maryland, September 24-26 1984 (pp. 294-311).
• The Security Model of Enhanced HDM by John Rushby. Proceedings 7th DoD/NBS Computer Security Conference, Gaithersburg, Maryland, September 24-26 1984 (pp. 120--136).

• A Distributed Secure System by John Rushby and Brian Randell, IEEE Computer, Vol. 16 no. 7, Jul 1983, pp. 55-67
• A Distributed Secure System, by John Rushby and Brian Randell, Technical Report 182, Computing Laboratory, University of Newcastle upon Tyne UK, May 1983 (longer version of the paper above)

• Proof of Separability---A Verification Technique for a Class of Security Kernels by John Rushby. Proceedings of the 5th International Symposium on Programming, Springer Verlag LNCS Vol. 137, pp. 352--367, Turin, Italy, 1982

• Design and Verification of Secure Systems, by John Rushby, from the 8th ACM Symposium on Operating System Principles, Pacific Grove, California, 14--16 December 1981.
• Verification of Secure Systems, by John Rushby, Technical Report 166, Computing Laboratory, University of Newcastle upon Tyne UK, August 1981

• LR(k) Sparse-Parsers and Their Optimization, PhD Thesis, University of Newcastle upon Tyne.

• FR80 Technical Papers, by John Rushby and others. Atlas Computer Laboratory, Chilton, UK, 1974-1975

• Formal Methods, Verification and Some Computing History: Interview with Wolfram Schulte at ICSE 2011 for Microsoft Channel 9. I was sitting too close to the camera (I won't make that mistake again), so I present a rather disturbing image of bulging teeth and eyes. You can avoid distress by just listening to the sound track: here's a direct link to the mp3 audio. Even though I say it myself, I think this is a pretty good presentation of SRI's historical contributions, and also the development and application of formal methods (as of 2011).
• After Dinner Speech at the Marktoberdorf Summer School, August 2010. This was recorded by one of the students. I weave parodies of the other lectures into an account of an interesting aviation incident (see this also), but I'm afraid the jokes might not work if you hadn't heard those lectures. I guess you had to be there.
• Youtube video of a talk at Fortiss in Munich in June 2017 on The Indefeasibility Criterion for Assurance Cases
• Introduction by John Lloyd and vimeo video of slides and voice over for an "Appreciation of some of Brian Randell's Contributions to Computer Security" on the occasion of his 75th birthday in May 2011.

If you're looking for slides from other talks, please scan through this directory listing, ordered by write date (and note the links at the bottom if you need format conversions)

2016

My lectures for the Marktoberdorf 2016 Summer School on Dependable Software Systems Engineering

• Lecture 1: Assurance and Formal Methods
• Lecture 2: Assurance Cases and their Arguments
• Lecture 3: Proofs and Assurance, The Case of The Ontological Argument
• Lecture 4: Formal Models for Human-Machine Interactions
• Lecture 5: Assurance in the Internet of Things And for Automated Driving

2015

• Consciousness and Rationality Explained Presentation for SRI's biweekly "Crazy Ideas" gathering, June 2015.

2011

• On the reliability of Monitored Systems Presented at Software Health Management Workshop, Palo Alto CA, 2 Aug 2011
• An Appreciation of Some of Brian Randell's Contributions to Computer Security Invited talk for Prof. Brian Randell's 75th Birthday Seminar
• What Is Assurance? Updated slides presented at Cambridge University, April 2011.

2010

• What Is Assurance? Invited talk for The Fourth Annual Layered Assurance Workshop (LAW 2010)
• Formal Methods and Argument-Based Safety Cases my lectures for the Marktoberdorf 2010 Summer School on Software and Systems Safety: Specification and Verification

2009

• Introduction to Static Analysis for Assurance presented at University of Minnesota Software Engineering Center Summer Software Symposium: Static Code Analysis and Complex Medical Devices
• Safety, Fault-tolerance, Verification, and Certification for Embedded Systems, guest lecture to EECS 149 at UC Berkeley, 13 April 2009

2008

• International Common Criteria Conference, Jeju, Korea, September 2008 High-Assurance Development and Evaluations: Rethinking the Common Criteria and EAL7, coauthored with Rance De Long
• Open Group Plenary, Chicago, July 2008 (MILS Policy Architectures)
• Software Certification Consortium, April 2008 (Safety Cases for Certification)
• NASA Langley Formal Methods Workshop, April 2008 (Formal Methods and Certification)
• NASA Fault Management Workshop, April 2008 (Evidence, Arguments, and Automation)

• 8th International Common Criteria Conference Compositional Security Evaluation: The MILS Approach, coauthored with Rance DeLong
• 8th International Common Criteria Conference A Common Criteria Authoring Environment Supporting Composition, coauthored with Rance DeLong
• HCMDSS & MD PnP, Boston, June 07 (Accidental Systems)
• HCSS, Baltimore, June 07 (this one is about MILS)
• NASA ESMD, Houston, April 07
• Open Group, Paris, April 07 (Scientific Certification)

Return to my home page.