SRI International Computer Science Laboratory

Recent Papers by John Rushby

Fast Links: 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?

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.

Preview copies of some papers that have not been published yet are available from this directory listing (ordered by file write date) and slides from this one (also ordered by write date)

I'm starting to provide html and epub versions of my papers. Only papers since 2012 are available in these formats at the moment. All tablets and ebook-readers (except Kindle, but does anyone use those?) can read epub right out of the box. Note that an ebook-reader (like the Nook) cannot download epub over the web (except from the B&N store): you need to download the epub file to a computer, then sideload it to the Nook over USB (how lame is that?).

I'm using TtH to translate LaTeX to (x)html (this works OK for fairly simple files) and Calibre to translate that to epub format. However, both the html and epub files fail validation and break some readers, so I have more work to do: most of the errors are due to hacks I made to fix other problems in the html file, and to the presence of & in BibTeX cites. And I haven't yet found a toolchain that can handle complex LaTeX files without some intervention; TeX4ht gets 95% of the way there and looks the most promising.

2012

• 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. Selected as the Spotlight Paper for the issue and available to the public for free for 30 days.
• 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, 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
• Formal Methods for Test Case Generation by John Rushby, Leonardo De Moura, and Grégoire 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

• 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.
• 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 Grégoire 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 the prepublication PDF version of the report for free here; it will cost money after the official publication date.
• 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 Grégoire Hamon, Leonardo de Moura, and John Rushby. CSL Technical Note, January 2005.

• Generating Efficient Test Sets with a Model Checker by Grégoire 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 Grégoire 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
• 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

• 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.

• 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

• 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. The citation history of this paper is interesting: it peaked 27 years after publication.

• 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
• 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, but I'm afraid the jokes might not work if you hadn't heard those lectures. I guess you had to be there.

• The Versatile Synchronous Observer Invited talk for 15th Brazilian Symposium on Formal Methods (SBMF), Natal, 25 Sep 2012

• 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: Specificaiton 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)

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)

Return to my home page.