Ricky W. Butler's Publications

1. George E. Hagen, Nelson M. Guerreiro, Jeffrey M. Maddalon, Ricky W. Butler. An effcient Universal Trajectory Language, NASA/TM-2017-219669, Sept 2017.

2. Guerreiro, Nelson M.; Jones, Denise R.; Barmore, Bryan E.; Butler, Ricky W.; Hagen, George E.; Maddalon, Jeffrey M.; Ahmad, Nash'at N.; Rogers, Laura J.; Underwood, Matthew C.; Johnson, Sally C. An Advanced Trajectory-Based Operations Prototype Tool and Focus Group Evaluation NASA/TM-2017-219670 Sept 2017.

3. Guerreiro, Nelson M., Jones, Denise R., Barmore, Bryan E., Butler, Ricky W., Hagen, George E., Maddalon, Jeffrey M., Ahmad, Nash'at N. Prototype Tool and Focus Group Evaluation for an Advanced Trajectory-Based Operations Concept, 17th AIAA Aviation Technology, Integration, and Operations Conference, AIAA AVIATION Forum, (AIAA 2017-4096)

4. Hagen, George E., Butler, Ricky W., Maddalon, Jeffrey M. The Stratway Program for Strategic Conflict Resolution: User's Guide , NASA/TM-2016-219196, May 2016.

5. Nelson M. Guerreiro, Ricky W. Butler, George E. Hagen, Jeffrey M. Maddalon, and Timothy A. Lewis Parametric Analysis of Surveillance Quality and Level and Quality of Intent Information and their Impact on Conflict Detection Performance, NASA/TM-2016-219177, March 2016.

6. Nelson M. Guerreiro, Ricky W. Butler , Jeffrey M. Maddalon , George E. Hagen , and Timothy A. Lewis, Conflict Detection Performance Analysis For Function Allocation Using Time-Shifted Recorded Traffic Data, June 22-26, 2015 in Dallas, Texas.

7. Aaron Dutle, César Muñoz, Anthony Narkawicz, and Ricky Butler, Software Validation via Model Animation, Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015), Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015. BibTeX Reference.
8. George E. Hagen and Ricky W. Butler, Towards a Formal Semantics of Flight Plans and Trajectories, NASA/TM-2014-218662, Dec 2014.
9. Wilfredo Torres-Pomales, Michael M. Madden, Ricky W. Butler, and Raleigh B. Perry, Analysis and Simulation of the Simplified Aircraft-Based Paired Approach Concept With the ALAS Alerting Algorithm in Conjunction With Echelon and Offset Strategies NASA/TM–2014-218151, Jan 2014.
10. Ricky W. Butler and Timothy A. Lewis, A Turn-Projected State-Based Conflict Resolution Algorithm, Technical Memorandum NASA/TM–2013-218055, November, 2013
11. Raleigh B. Perry, Michael M. Madden, Wilfredo Torres-Pomales, Ricky W. Butler. The Simplified Aircraft-Based Paired Approach With the ALAS Alerting Algorithm, Technical Memorandum NASA/TM-2013-217804, February, 2013
12. Ricky W. Butler, George Hagen, and Jeffrey M. Maddalon, The Chorus Conflict and Loss of Separation Resolution Algorithms, Technical Memorandum NASA/TM-2013-218030, August 2013.
13. Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, and Anthony Narkawicz, The search for effective algorithms for recovery from loss of separation, Proceedings of the 31st Digital Avionics Systems Conference (DASC 2012), Williamsburg, Virginia, 2012. BibTeX Reference.
14. Hagen, G. E.; Butler, R. W.; and Maddalon, J. M.: Stratway: A Modular Approach to Strategic Conflict Resolution. Presented at 11th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, September 20-22, 2011, Virginia Beach, Virginia.

15. César Muñoz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen, A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing the Safety of Self-Separation in NextGen, Technical Memorandum, NASA/TM-2010-216862, October 2010. BibTeX Reference.
16. Ricky W. Butler; George Hagen; Jeffrey M. Maddalon; Cesar A. Munoz; Anthony Narkawicz; How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project, Second NASA Formal Methods Symposium (NFM 2010), Washington D.C., April 13-15, 2010.
17. Jeffrey Maddalon, Ricky Butler, Cesar Munoz, Gilles Dowek.  A Mathematical Analysis of Conflict Prevention Information.   Presented at the 9th Aviation Technology, Integration, and Operations Conference (ATIO), AIAA-2009-6907. Sept 21st, 2009, Hilton Head, SC.  PDF
18. Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009. BibTex Reference.
19. Butler, Ricky W.; Munoz, Cesar A. Formally Verified Practical Algorithms For Recovery From Loss of Separation , NASA TM-2009-215726, June 2009.
20. Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover , Journal of Formalized Reasoning, Vol 2, No 1., 2009.
21. Butler, Ricky W.; Munoz, Cesar A. A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation , NASA TM-2008/215356, Oct 2008.
22. Radu Siminiceanu, Ricky W. Butler, César Muñoz. Experimental Evaluation of a Planning Language Suitable for Formal Verification", Model Checking and Artificial Intelligence 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008; Lecture Notes in Computer Science, Springer Berlin, Volume 5348/2009.
23. Ricky W. Butler, César Muñoz. NASA Langley's Formal Methods Research in Support of the Next Generation Air Transportation System Proceedings of The Sixth NASA Langley Formal Methods Workshop, June 2008, p.3-5.
24. Ricky W. Butler, A Primer on Architectural Level Fault Tolerance, NASA TM-2008-215108, Feb 2008.
25. Ricky Butler, Radu Siminiceanu and César Muñoz, The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM-2007-215088, Nov 2007.
26. Ricky Butler, César Muñoz, and Radu Siminiceanu, Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL), NASA/TM-2007-215089 , Nov 2007.
27. Ricky Butler and César Muñoz, An Abstract Plan Preparation Language, NASA/TM-2006-214518, Nov 2006.
28. Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover , NASA TM-2004-213279,Oct-2004.
29. Jeffrey Maddalon, Ricky Butler, Alfons Geser and Cesar Munoz, Formal Verification of a Conflict Resolution and Recovery Algorithm , NASA/TP-2004-213015, April 2004, pp. 82.
30. Victor A. Carreno, Hanne Gottliebsen, Ricky Butler and Sara Kalvala, Formal Modeling and Analysis of a Preliminary Small Aircraft Transportation System (SATS) Concept, NASA/TM-2004-212999, March 2004, pp. 44.
31. Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz: Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings of Winter Simulation Conference (WSC'03), New Orleans, December 2003, pp. 906-914, ISBN 0-7803-8132-7.
32. R.W. Butler; V. Carreno; G. Dowek and C. Munoz: Formal Verification of Conflict Detection Algorithms , Proceedings of the 11th Working Conference on Correct Hardware Design and Verification Methods CHARME 2001}, Lecture Notes in Computer Science, Vol. 2144, p. 403-417, 2001, Livingston, Scotland, UK. (Postscript, 15 pages). Also published in the International Journal on Software Tools for Technology Transfer in 2003.

33. Johnson, Sally C.; and Butler, Ricky W.;: Formal Methods, Chapter 21 in The Avionics Handbook, edited by Cary R. Spitzer, CRC Press, 2001

34. Cesar Munoz; Ricky W. Butler; Victor A. Carreno; and Gilles Dowek, On the Formal Verification of Conflict Detection Algorithms, NASA/TM-2001-210864, May 2001.

35. Butler, Ricky W., WinSURE: A New Windows Interface to the SURE Program , 19th Digital Avionics Systems Conference; Oct 7-13, 2000 Philadelphia, PA.

36. Butler, Ricky W., Miller; Steven P., Potts, James N.; and Carreno, Victor A.: A Formal Methods Approach to the Analysis of Mode Confusion , 17th Digital Avionics Systems Conference, Bellevue, Washington, October 31--November 6, 1998.

37. Ricky W. Butler, Kelly J. Hayhurst and Sally C. Johnson, A Note About HARP's State Trimming Methods, NASA/TM-1998-208427, May 1998.

38. Butler, Ricky W. and Sjogren, Jon A.: A PVS Graph Theory Library, NASA Technical Memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia, Feb 1998. 24 pages)

39. Butler, Ricky W.; Miner, Paul S.; Srivas, Mandayam K.; Greve, Dave A.; and Miller, Steven P.: A Bitvectors Library For PVS, Aug 1996, NASA TM-110274.

40. Butler, Ricky W. An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. NASA Technical Memorandum 111025, NASA Langley Research Center, Hampton, Virginia, May 1996. 32 pages, 257246 bytes)

41. Holloway, C. Michael; Butler, Ricky W.: Impediments to Industrial Use of Formal Methods, in IEEE Computer, April 1996, pp. 25-26.

42. Butler, Ricky W.; and Johnson, Sally C.: Techniques for Modeling the Reliability of Fault-Tolerant Systems Using the Markov State-Space Approach , NASA RP-1348, Sept 1995. ( 112 pages, 1115955 bytes)

43. Butler, Ricky W.; Di Vito, Ben L.; and Holloway C. Michael: Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 3 Results). NASA Technical Memorandum 109140, NASA Langley Research Center, Hampton, Virginia, August 1994. (PostScript, 112 pages, 1115955 bytes)

44. Butler, Ricky W.; Caldwell, James L.; Carreno, Victor A.; Holloway, C. Michael; Miner, Paul S.; and Vito, Ben L. Di: NASA Langley's Research and Technology Transfer Program in Formal Methods. In Tenth Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995. (PostScript, 15 pages; updated version PostScript, 37 pages)

45. Divito, Benedetto L.; and Butler, Ricky W.: Formal Techniques for Synchronized Fault-Tolerant Systems. In Dependable Computing and Faul-Tolerant Systems , Vol. 8, C. E. Landwehr, B. Randell, L. Simoncini, eds., 1993, p. 163-188. (Book) 12 pages)

46. Butler, Ricky W.; and Johnson, Sally C.: Formal Methods For Life-Critical Software . In Computing in Aerospace 9 Conference , pages 319-329, San Diego, California, October 1993.

47. Butler, Ricky W.: An Elementary Tutorial on Formal Specification and Verification Using PVS . NASA Technical Memorandum 108991, NASA Langley Research Center, Hampton, Virginia, September 1993. Revised in 1995. (

48. Butler, Ricky W.; and Finelli, George B.: The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, 19(1):3-12, January 1993. ( PDF , 11 pages)

49. Di Vito, Benedetto L.; Butler, Ricky W.; and Caldwell, James L.: High Level Design Proof of a Reliable Computing Platform. In Dependable Computing for Critical Applications 2, J. F. Meyer and R. D. Schlichting, eds., p. 279-306, 1992. (PostScript, 12 pages)

50. Di Vito, Benedetto L.; and Butler, Ricky W.: Formal Techniques for Synchronized Fault-Tolerant Systems . In Dependable Computing for Critical Applications 3, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1993. Also presented at 3rd IFIP Working Conference on Dependable Computing for Critical Applications, Mondello, Sicily, Italy, Sept. 14-16, 1992. (PostScript, 13 pages, 222753 bytes)

51. Di Vito Benedetto L.; Butler, Ricky W.; and Caldwell, James L.: High Level Design Proof of a Reliable Computing Platform. In Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1992. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, Arizona, Feb. 18-20, 1991, pp. 124-136. (PostScript, 13 pages, 209527 bytes)

52. Di Vito, Benedetto L.; and Butler, Ricky W.: Provable Transient Recovery for Frame-Based, Fault-Tolerant Computing Systems. In Real-Time Systems Symposium, Phoenix, Arizona, December 1992. ( PostScript, 4 pages, 103167 bytes)

53. Johnson, Sally C.; Holloway, C. Michael; Butler, Ricky W.: Second NASA Formal Methods Workshop 1992. NASA Conference Publication 10110, NASA Langley Research Center, Hampton, Virginia, November 1992.

54. Johnson, Sally C.; and Butler, Ricky W.: A Table-Oriented Interface for Reliability Modeling of Fault-Tolerant Architectures. Presented at the 11th Digital Avionics Systems Conference, Seattle, WA, October 5-8, 1992. In Proceedings, pg. 149-154.

55. Butler, Ricky W.: The SURE Approach to Reliability Analysis. IEEE Transactions on Reliability, Vol. 41, No. 2, p. 210-218, June 1992. (Program available here.)

56. Johnson, Sally C.; and Butler, Ricky W.: Design for Validation. IEEE Aerospace Electronic Systems, January 1992, Vol. 7, No. 1, p. 38-43 (PostScript, 6 pages)

57. Butler, Ricky W.; and Di Vito, Ben L.: Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 2 Results) . NASA Technical Memorandum 104196, NASA Langley Research Center, Hampton, Virginia, January 1992. (PostScript, 68 pages, 524562 bytes)

58. Johnson, Sally C.; and Butler, Ricky W.: Design For Validation . IEEE Aerospace and Electronics Systems, pages 38-43, January 1992. Also appeared in the AIAA/IEEE 10th Digital Avionics Systems Conference, Los Angeles, California, Oct. 7-11, 1991, pp. 487-492. (PostScript, 6 pages, 113097 bytes)

59. Butler, Ricky W. and Sjogren, Jon A.: Formal Design Verification of Digital Circuitry. Reliability Engineering and System Safety, Vol. 32, p. 67-93, 1991.

60. Butler, Ricky W.; and Finelli, George B.: The Infeasibility of Experimental Quantification of Life-Critical Software Reliability. Presented at the ACM SIGSOFT '91 Conference on Software for Critical Systems, New Orleans, LA, December 4-6, 1991. In Proceedings, Vol. 16, No. 5, p. 66-76.

61. Butler, Ricky W.: NASA Langley's Research Program in Formal Methods. Presented at the IEEE Sixth Annual Conference on Computer Assurance Systems Integrity, Software Safety, and Process Security (COMPASS '91), Gaithersburg, MD, June 25-27, 1991.

62. Butler, Ricky W.; Caldwell, James L.; and Di Vito, Ben L.: Design Strategy for a Formally Verified Reliable Computing Platform. Presented at the IEEE Sixth Annual Conference on Computer Assurance Systems Integrity, Software Safety, and Process Security (COMPASS '91), Gaithersburg, MD, June 25-27, 1991. In Proceedings, p. 125-133. (PostScript)

63. Butler, Ricky W. (Ed.). NASA Formal Methods Workshop 1990 . NASA CP-10052, November 1990.

64. Ramanathan, P.; Shin, K. G.; and Butler, Ricky W.: Fault-Tolerant Clock Synchronization in Distributed Systems . IEEE Computer, October 1990, Vol. 23, No. 10, p. 33-42.

65. Di Vito, Ben L.; Butler, Ricky W.; and Caldwell, James L.: Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 1 Results). NASA Technical Memorandum 102716, NASA Langley Research Center, Hampton, Virginia, October 1990. (PostScript, 68 pages, 461037 bytes)

66. Caldwell, James L., II; Butler, Ricky W.; and Di Vito, Ben L.: Hierarchical Approach to Specification and Verification of Fault-Tolerant Operating Systems. Presented at the Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA, July 17-19, 1990, Pacifica, CA. In Proceedings.

67. Butler, Ricky W.; and Johnson, Sally C.: The Art of Fault-Tolerant System Reliability Modeling. NASA TM-102623, March 1990.

68. Butler, Ricky W.; and Martensen, Anna L.: The Fault-Tree Compiler (FTC) Program and Mathematics. NASA TP-2915, July 1989. (Program available here.)

69. Butler, Ricky W.; and Sjogren, Jon A.: Hardware Proofs Using EHDM and the RSRE Verification Methodology. NASA Technical Memorandum 100669, NASA Langley Research Center, Hampton, Virginia, December 1988.

70. Butler, Ricky W.: Fault-Tolerant Clock Synchronization Techniques for Avionics Systems. Presented at the AIAA/AHS/ASEE Aircraft Design and Operations Meeting, Atlanta, GA, September 7-9, 1988. AIAA Paper No. 88-4408.

71. Butler, Ricky W.; and White, Allan L.: SURE Reliability Analysis Program and Mathematics. NASA TP-2764, March 1988. (Program available here.)

72. Butler, Ricky W.; and Stevenson, Phillip H.: The Paws and Stem Reliability Analysis Programs, NASA TM-100572, March 1988. (Program available here.)

73. Butler, Ricky W.: A Survey of Provably Correct Fault-Tolerant Clock Synchronization Techniques, NASA TM-100553, February 1988.

74. Johnson, Sally C.; and Butler, Ricky W.: Automated Generation of Reliability Models. Presented at the ASME, ASQC, et al., 1988 Annual Reliability and Maintainability Symposium, Los Angeles, CA, January 26-28, 1988. In Proceedings, p. 17-22.

75. Butler, Ricky W.; Palumbo, Daniel L.; and Johnson, Sally C.: Fault-Tolerant Clock Synchronization Validation Methodology. Journal of Guidance, Control, and Dynamics, Vol. 10, No. 6, p. 513-522, November-December 1987.

76. Ellis, Erik L.; and Butler, Ricky W.: Estimating the Distribution of Fault Latency in a Digital Processor. NASA TM-100521, November 1987.

77. Butler, Ricky W.; and Elks, Carl R.: A Preliminary Transient-Fault Experiment on the SIFT Computer System. NASA TM-89058, February 1987.

78. Martensen, Anna L.; and Butler, Ricky W.: The Fault-Tree Compiler. NASA TM-89098, January 1987.

79. Butler, Ricky W.: An Abstract Language for Specification of Markov Reliability Models. IEEE Transactions on Reliability , Vol. R-35, No. 5, p. 595-601, December 1986. (Program available here.)

80. Butler, Ricky W.: The SURE Reliability Analysis Program. Presented at the AIAA Guidance, Navigation and Control Conference, Williamsburg, VA, August 18-20, 1986. AIAA Paper No. 86-2034-CP. (Program available here.)

81. Palumbo, Daniel L.; and Butler, Ricky W.: A Performance Evaluation of the Software-Implemented Fault-Tolerance Computer . Journal of Guidance, Control, and Dynamics, Vol. 9, No. 2, p. 175-180, March-April 1986.

82. Butler, Ricky W.: The SURE Reliability Analysis Program. NASA TM-87593, February 1986.

83. Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Ensuring Fault-Tolerance of Phased-Locked Clocks . IEEE Transactions on Computers, Vol. C-34, p. 752-756, August 1985.

84. Butler, Ricky W.; Palumbo, Daniel L.; and Johnson, Sally C.: Application of a Clock Synchronization Validation Methodology to the SIFT Computer System. Presented at the IEEE Fifteenth International Symposium on Fault-Tolerant Computing, Ann Arbor, MI, June 19-21, 1985. IEEE Paper No. 64.

85. Palumbo, Daniel L.; and Butler, Ricky W.: Measurement of SIFT Operating System Overhead. NASA TM-86322, April 1985.

86. Butler, Ricky W.: An Abstract Specification Language for Markov Reliability Models. NASA TM-86423, April 1985. (Program available here.)

87. Johnson, Sally C.; and Butler, Ricky W.: Validation of a Fault-Tolerant Clock Synchronization System. Presented at the AIAA/IEEE 6th Digital Avionics Systems Conference, Baltimore, MD, December 3-6. 1984. AIAA Paper No. 84-2648-CP.

88. Butler, Ricky W.; and Johnson, Sally C.: Validation of a Fault-Tolerant Clock Synchronization System. NASA TP-2346, September 1984.

89. Butler, Ricky W.: The Semi-Markov Unreliability Range Evaluator (SURE) Program. NASA TM-86261, July 1984.

90. Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Synchronization and Fault-Masking in Redundant Real-Time Systems presented by Butler at the Fourteenth International Conference on Fault-Tolerant Computing, Kissimmee, FL, June 20-22, 1984. In Proceedings, p. 152-157.

91. Butler, Ricky W.: Critical Issues in Real-Time Operating Systems. Presented at the IEEE 1983 Real-Time Systems Symposium, Arlington, VA, December 7, 1983.

92. Palumbo, Daniel L.; and Butler, Ricky W.: SIFT - A Preliminary Evaluation. Presented at the IEEE/AIAA 5th Digital Avionics Systems Conference, Seattle, WA, October 31-November 3, 1983. IEEE/AIAA Paper No. 21.4.

93. Butler, Ricky W.: Fault-Tolerant Operating Systems Research in AIRLAB. Presented at the IEEE Computer Society Workshop on Laboratories for Reliable Systems Research, Hampton, VA, April 27-29, 1983.

94. Butler, Ricky W.: An Assessment of the Real-Time Application Capabilities of the SIFT Computer System. Presented at the General Electric Company Second Annual Reliable and Fault-Tolerant System Seminar, Charlottesville, VA, April 20, 1983. (Available as NASA TM-84482).

95. Butler, Ricky W.: An Assessment of the Real-Time Application Capabilities of the SIFT Computer System. NASA TM-84482, April 1982.