SRI International Computer Science Laboratory

Recent Papers by John Rushby

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

Links to slides; Links to papers by my colleagues; Link to our top-level formal methods page

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.

The links below give access to abstracts and BibTeX entries for my papers and to pdf, postscript, or dvi copies of the papers themselves. Note: not all papers are available in all formats. Links to missing papers will be added when the final versions are available (if copyright restrictions allow)

2007

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.

2006

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.

2005

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.

2004

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.

2002

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.

2001

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.

2000

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

1999

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.

1998

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.

1997

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.

1996

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

1995

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

1994

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

1993

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.

1992

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

1991

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

1989

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

1988

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

1986

(I'm slowly getting my old papers online)

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

1985

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.

1984

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

1983

A Distributed Secure System by John Rushby and Brian Randell, IEEE Computer, Vol. 16 no. 7, Jul 1983, pp. 55-67

1982

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

1981

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

1977

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

1974

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

Slides

Slides given in association with a published paper are available from the link to the paper concerned. Here are links to PDFs for a few recent talks (newest first) that are not associated with a paper:

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)
Runtime Verification, at ETAPS 2008 (Runtime Certification)
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 (and note the links at the bottom if you need format conversions)

Return to my home page.

John Rushby (Rushby@csl.sri.com)