SRI International Publications

See SRI's World Wide Web server for an up-to-date list of SRI publications and electronic versions of many of them. The list here may not be complete.

1. Rushby, John: Partitioning in Avionics Architectures: Requirements Mechanisms, and Assurance. NASA CR-1999-209347, June 1999.
2. Owre, Sam and Shankar Natarajan: The Formal Semantics of PVS. NASA/CR-1999-209321, May 1999.
3. Owre, Sam and Shankar Natarajan: Abstract Datatypes in PVS. NASA/CR-97-206264, November 1997.
4. Owre, Sam; Rushby, John; and Shankar Natarajan: Analyzing Tabular and State-Transition Requirements Specifications in PVS. NASA CR-201729, July 1997.

5. Rushy, John: A Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model. NASA Contractor Report 198289, March 1996.

6. Rushby, John: Formal Methods and Their Role in Digital Systems Validation for Airborne Systems. NASA Contractor Report 4673, August 1995. (This is a shorter and somewhat less technical treatment of the subjects addressed in NASA CR 4551 below. SRI has a technical report similar to this paper.)

7. Srivas, Mandayam K.; and Miller, Steven P: Formal Verification of an Avionics Microprocessor. NASA Contractor Report 4682, August 1995.

8. Miller, Steven P; and Srivas, Mandayam: Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods, Presented at WIFT '95: Workshop on Industrial-Strength Formal Specif WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, April 5-8, 1995, Boca Raton, Florida USA, pp. 30-43.

9. Crow, Judy; and Rushby, John: Model-Based Reconfiguration: Diagnosis and Recovery, NASA Contractor Report 4596, May 1994.

10. Rushby, John: Formal Methods and Digital Systems Validation for Airborne Systems. NASA Contractor Report 4551, December 1993.

11. Rushby, John: A Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. In Vytopil, Jan, editor 1993:, Formal Techniques in Real-Time and Fault-Tolerant Systems, Kluwer International Series in Engineering and Computer Science, chapter 5, pp. 109-136. Kluwer, Boston, Dordecht, London, 1993.

12. Rushby, John; and Srivas, Mandayam: Using PVS to Prove Some Theorems of David Parnas. In Proceedings of the 1993 International Workshop on the HOL Theorem Proving System and its Applications, Vancouver, Canada, Aug. 1993.

13. Lincoln, Patrick; and Rushby, John: A Formally Verified Algorithm For Interactive Consistency Under a Hybrid Fault Model. NASA Contractor Report 4527, July 1993.

or Report 4527, July 1993.
14. Lincoln, Patrick; and Rushby, John: Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. In Courcoubetis, Costas, editor 1993:, Computer Aided Verification, CAV '93, vol. 697 of Lecture Notes in Computer Science, Elounda, Greece, June/July 1993, Springer Verlag, pp. 292-304.

15. Lincoln, Patrick; and Rushby, John: A Formally Verified Algorithm for Interactive Consistency under a Hybrid Fault Model. In Fault Tolerant Computing Symposium 23, Toulouse, France, June 1993, IEEE Computer Society, pp. 402-411.

16. Owre, Sam; Rushby, John; Shankar, Natarajan; and von Henke, Friedrich: Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. In Woodcock, J. C. P.; and Larsen, P. G., editors 1993:, FME '93: Industrial-Strength Formal Methods, vol. 670 of Lecture Notes in Computer Science, Odense, Denmark, Apr. 1993, Springer Verlag, pp. 482-500.

17. Rushby, John; and von Henke, Friedrich: Formal Verification of Algorithms for Critical Systems. IEEE Transactions on Software Engineering, vol. 19, no. 1, Jan. 1993, pp. 13-23.

18. Owre, S.; Rushby, J. M.; and Shankar, N.: PVS: A Prototype Verification System. In Kapur, Deepak, editor 1992:, 11th International Conference on Automated Deduction (CADE), vol. 607 of Lecture Notes in Artificial Intelligence, Saratoga, NY, June 1992, Springer Verlag, pp. 748-752.

19. Shankar, Natarajan: Mechanical Verification of a Generalized Protocol for Byzantine Fault-Tolerant Clock Synchronization. In Second International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, vol. 571 of Lecture Notes in Computer Science, pp. 217-236. Springer Verlag, Nijmegen, The Netherlands, Jan. 1992.

20. Rushby, John: Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. In Second International Symposium o> Second International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, vol. 571 of Lecture Notes in Computer Science, pp. 237-258. Springer Verlag, Nijmegen, The Netherlands, Jan. 1992.

21. Vytopil, J., editor 1992: Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 571 of Lecture Notes in Computer Science, Nijmegen, The Netherlands, Jan. 1992. Springer Verlag.

22. Rushby, John; and von Henke, Friedrich: Formal Verification of Algorithms for Critical Systems. In SIGSOFT '91: Software for Critical Systems, New Orleans, LA, Dec. 1991, pp. 1-15. Published as ACM SIGSOFT Engineering Notes, Volume 16, Number 5, selected for a special issue of IEEE TSE for January 93.

23. Rushby, John: Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. NASA Contractor Report 4384, July 1991.

24. Shankar, Natarajan: Mechanical Verification of a Schematic Byzantine Clock Synchronization Algorithm. NASA Contractor Report 4386, July 1991.

25. Crow, Judith; and Rushby, John: Model-Based Reconfiguration: Toward an Integration with Diagnosis. In Integration with Diagnosis. In Proceedings, AAAI-91 (Volume 2), Anaheim, CA, July 1991, pp. 836-841.

26. Rushby, John; and Crow, Judith: Evaluation of an Expert System for Fault Detection, Isolation, and Recovery in the Manned Maneuvering Unit. NASA Langley Research Center, Contractor Report 187466, Hampton, VA, Dec. 1990. (Work performed by SRI International).

27. Rushby, John: Validation and Testing of Knowledge-Based Systems: How Bad can it get? In Proceedings of AAAI 88 Workshop on Validation and Testing Knowledge-Based Systems, Saint Paul, MN, August 1988. Reprinted in Validating and Verifying Knowledge-Based Systems, IEEE Computer Society, 1991.

28. Rushby, John; and von Henke, Friedrich: Formal Verification of a Fault-Tolerant Clock Synchronization Algorithm. NASA Contractor Report 4239, June 1989.

29. Rushby, John; and Whitehurst, R. Alan: Formal Verification of AI Software. NASA Contractor Report 181827, Feb. 1989.