% This is the bibliographic database in bibtex format for NASA LaRC FM  
% Publications IT IS NOT UP TO DATE
@string{CR = "{NASA} Contractor Report"}
@string{CP = "{NASA} Conference Publication"}
@string{TM = "{NASA} Technical Memorandum"}
@string{TP = "{NASA} Technical Paper"}
@string{ieeetse = {IEEE Transactions on Software Engineering}}
@string{larc = {NASA Langley Research Center, Hampton, Virginia}}

@TechReport{ detmode,
  author = {Steven P. Miller and James N. Pott},
  title = {{Detecting Mode Confusion Through
Formal Modeling and Analysis}},
  month = jan,
  year = 1999,
  institution = larc,
  number = {{CR-1999-208971}},
  keywords = {PVS, partitioning, avionics, IMA },
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2279/1=techreports.larc.nasa.gov%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202279%20/usr/local/web/htdocs/ltrs/refer/1999/cr/NASA-99-cr208971.refer.html;4=techreports.larc.nasa.gov%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202279%20/usr/local/web/htdocs/ltrs/refer/1999/cr/NASA-99-cr208971.refer.html;7=%00; },                
  type = CR
}


@InProceedings{ButlerDASC98,
  author =       "Ricky W. Butler and Steven P. Miller and James N. Potts and Victor A. Carre{\~{n}}o",
  title =        {{A Formal Methods Approach to the Analysis of Mode Confusion}}, 
  pages =        "",
  booktitle =    "17th AIAA/IEEE Digital Avionics Systems Conference",
  year =         "1998",
  month =        "October 31 -  November 6",
  city =         {Bellevue, Washington},                  
  postscript={ftp://air16.larc.nasa.gov/pub/fm/papers/1998/butler-etal-dasc98.ps},
  note={<a href="papers/butler-etal-dasc98.pdf">PDF</a>}
}

@TechReport{ BenIMA,
  author = {Ben L. {Di Vito}},
  title = 	 {{A Formal Model of Partitioning for Integrated Modular Avionics}},
  month = aug,
  year = 1998,
  institution = larc,
  number = {{CR-1998-208703}},
  keywords = {PVS, partitioning, avionics, IMA },
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2303/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202303%20/usr/local/web/htdocs/ltrs/refer/1998/cr/NASA-98-cr208703.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202303%20/usr/local/web/htdocs/ltrs/refer/1998/cr/NASA-98-cr208703.refer.html;7=%00; },                
  type = CR
}

@techreport{GCS,
  author ="Kelly J. Hayhurst",
  title = {{Framework for Small-Scale Experiments in Software Engineering}},
  month = {May},
  year = 1998,
  institution=larc,
  type=TM,
  number= {TM-1998-207666},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2453/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202453%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-tm207666.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202453%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-tm207666.refer.html;7=%00;},
}


@techreport{SSAC-WSI,
  author = "K. J. Hayhurst and C. M. Holloway and C. A. Dorsey and
                  J. C. Knight and N. G. Leveson and G. F. McCormick and
                  J. C. Yang",
  title = {{Streamlining Software Aspects of Certification: Technical Team
                  Report on the First Industry Workshop}}, 
  month = {April}, 
  year = 1998,
  institution = larc,
  number = {TM-1998-207648},
  type = TM,
  note = {Information on the SSAC project is <a
                  href="http://shemesh.larc.nasa.gov/ssac/">here</a>.},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2325/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202325%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-cr207648.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202325%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-cr207648.refer.html;7=%00;},
}
                  
@TechReport{ButlerGraph,  
  author = 	 "Ricky W. Butler and J. A. Sjogren",
  title = 	 {{A PVS Graph Theory Library}},
  month = feb,
  year = 1998,
  institution = larc,
  number = {TM-1998-206923},
  keywords={Graphs, Formal methods, PVS libraries, Formal proof },
  type = TM,
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1267/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201267%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-tm206923.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201267%20/usr/local/web/htdocs/ltrs/refer/1998/tm/NASA-98-tm206923.refer.html;7=%00;},                
}
                  
@InProceedings{HollowayDASC97,
  author =       "C. Michael Holloway",
  title =        {{Why Engineers Should Consider Formal Methods}},
  pages =        "1.3-16 -- 1.3-22",
  booktitle =    "16th AIAA/IEEE Digital Avionics Systems Conference, Volume 1",
  year =         "1997",
  month =        "October 26-30",
  city =         {Irvine, California},                  
  note =         {Presentation slides are <a href="http://shemesh.larc.nasa.gov/~cmh/DASC97/">available</a>},
  postscript={/~cmh/DASC97/dasc97-paper.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1483/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201483%20/usr/local/web/htdocs/ltrs/refer/1997/mtg/NASA-97-16dasc-cmh.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201483%20/usr/local/web/htdocs/ltrs/refer/1997/mtg/NASA-97-16dasc-cmh.refer.html;7=%00;},
}

@techreport{Holloway-FM-wkshp-IV,
  author = "C. Michael Holloway and Kelly J. Hayhurst (compilers)",
  title = {{Lfm97: Fourth NASA Formal Methods Workshop}},
  month = {September}, year = 1997,
  institution = larc,
  number = 3356,
  url = {http://shemesh.larc.nasa.gov/Lfm97/proceedings/}, 
  keywords = {workshop, technology transfer, hardware, software,
		  requirements, proofs, design}, 
  type = CP
}

@TechReport{ GPS,
  author = {Ben L. {Di Vito}},
  title = 	 {{Using Formal Methods to Assist in the Requirements
                  Analysis of the Space Shuttle GPS Change Request}},
  month = aug,
  year = 1996,
  institution = larc,
  number = 4752,
  keywords = {PVS, requirements, software, GPS, shuttle},		  
  type = CR,
  url = {http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2282/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202282%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-96-cr4752.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202282%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-96-cr4752.refer.html;7=%00;},                 
}
                  
@TechReport{Autopilot,
  author = 	 "Ricky W. Butler",
  title = 	 {{An Introduction to Requirements Capture Using PVS:
		  Specification of a Simple Autopilot}},
  month = may,
  year = 1996,
  institution = larc,
  number = 111025,
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1996/autopilot-pvs.ps},
  keywords = {PVS, requirements, software},		  
  type = TM,
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1730/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201730%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-96-tm110255.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201730%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-96-tm110255.refer.html;7=%00;},                
}

@Article{Roundtable,
  author = 	 "C. Michael Holloway and Ricky W. Butler",
  title = 	 {{Impediments to Industrial Use of Formal Methods}},
  journal =	 "IEEE Computer",
  year =	 "1996",
  pages =	 "25-26",
  month =	 "April",
  volume =        29,
  number =       4,                 
  url =          {http://shemesh.larc.nasa.gov/fm/fm-paper-ieee-roundtable.html},
  keywords = {technology transfer, industry},		  
  postscript =   {ftp://air16.larc.nasa.gov/pub/fm/papers/1996/roundtable.ps}
}

@inproceedings{DiVito-FME96,
  author = {Ben L. {Di Vito}},
  title = {{Formalizing New Navigation Requirements for NASA's Space Shuttle}},
  month = Mar, days = {20--22},
  year = 1996,
  booktitle = {{Formal Methods Europe (FME '96)}},
  pages = {160--178},
  address = {Oxford, England},
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1996/fme96.ps},
  keywords = {Space, Shuttle, requirements, PVS},		  
  note = {Also Lecture Notes in Computer Science 1051, Springer},
  url = {http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1982/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201982%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-fme-96-bld.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201982%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-fme-96-bld.refer.html;7=%00;},                
}

@inproceedings{Crow-DiVito-shuttle,
  author = {Judith Crow and Ben L. {Di Vito}},
  title = {{Formalizing Space Shuttle Software Requirements}},
  month = Jan, days = {10--11},
  year = 1996,
  booktitle = {{Workshop on Formal Methods in Software Practice (FMSP '96)}},
  pages = {40--48},
  address = {San Diego, California},
  keywords = {Space, Shuttle, PVS, requirements},		  
  postscript={ftp://air16.larc.nasa.gov/pub/fm/papers/1996/fmsp96.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1729/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201729%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-fmsp-96-jc.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201729%20/usr/local/web/htdocs/ltrs/refer/1996/NASA-fmsp-96-jc.refer.html;7=%00;},                   
}

@InProceedings{HollowayDASC,
  author =       "C. Michael Holloway",
  title =        {{Ada 95 and Safety-Critical Software}},
  pages =        "504--509",
  booktitle =    "14th AIAA/IEEE Digital Avionics Systems Conference",
  year =         "1995",
  month =        "November",
  note =         {Presentation slides are <a
                  href="http://shemesh.larc.nasa.gov/~cmh/DASC95/">available</a>},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1790/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201790%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-dasc-95-cmh.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201790%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-dasc-95-cmh.refer.html;7=%00;},
}

@TechReport{CarrenoIEEEFP,
  author = 	 "Victor A. Carre{\~{n}}o",
  title = 	 {{Interpretation of IEEE-854 Floating-Point Standard and
		  Definition in the HOL System}},
  month = sep,
  year = 1995,
  institution = larc,
  number = 110189,
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1995/ieee854_hol.ps},
  keywords = {hardware, HOL, floating point, proofs},		  
  type = TM,
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1523/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201523%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-95-tm110189.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201523%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-95-tm110189.refer.html;7=%00;},                
}

@techreport{Holloway-FM-wkshp-III,
  author = "Holloway, (editor), C. Michael",
  title = {{Third NASA Formal Methods Workshop 1995}},
  month = {June}, year = 1995,
  institution = larc,
  number = 10176,
  url = {http://shemesh.larc.nasa.gov/WS95/proceedings.html}, 
  keywords = {workshop, technology transfer, hardware, software,
		  requirements, proofs, design}, 
  type = CP
}
		  
@techreport{MinerIEEEFP,
  author = "Paul S. Miner",
  title = {{Defining the IEEE-854 Floating-Point Standard in PVS}},
  month = {June}, year = 1995,
  institution = larc,
  number = 110167,
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1995/TM-110167.ps}, 
  keywords = {hardware, floating point, PVS, proofs},		  
  type = TM,
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1669/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201669%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-95-tm110167.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201669%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-95-tm110167.refer.html;7=%00;},                 
}

@inproceedings{Compass95,
  author = "Ricky W. Butler and James L. Caldwell and Victor
		  A. Carre{\~{n}}o and C. Michael Holloway and Paul S. Miner
		  and Ben L. {Di Vito}", 
  title = {{NASA Langley's Research and Technology Transfer Program in
		  Formal Methods}}, 
  month = Jun, days = "26--30",
  year = 1995,
  booktitle = "Tenth Annual Conference on Computer Assurance (COMPASS 95)",
  address = "Gaithersburg, MD",
  postscript={ftp://air16.larc.nasa.gov/pub/fm/papers/1995/compass95.ps},
  keywords = {technology transfer, overview},		  
  note={<a href="ftp://air16.larc.nasa.gov/pub/fm/papers/1996/NASA-fm-prg-overview.ps">An expanded version
		  is viewable here</a>}, 
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1964/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201964%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-ieee-95-compassrwb.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201964%20/usr/local/web/htdocs/ltrs/refer/1995/NASA-ieee-95-compassrwb.refer.html;7=%00;},                
}
		  
@InProceedings{triada94,
  author = 	 "C. Michael Holloway and Ben {Di Vito} and David Guaspari
		  and Michael Smith",
  title = 	 {{Formal Methods: Fact vs. Fiction}},
  booktitle = "Tri-Ada '94",
  year =	 1994,
  month =	 nov,
  note =	 "Panel Summary and Position Papers",
  keywords = {Ada, myths, technology transfer},		  
  url = 	 {paper-tri-ada.html}
}

@InProceedings{HollowayEPSEFM,
  author = 	 "C. Michael Holloway",
  title = 	 {{Epistemology, Software Enginering, and Formal Methods}},
  pages =	 "570-595",
  booktitle =	 "The Role of Computers in Research and Development at
		  Langley Research Center",
  year =	 "1994",
  month =	 "October",
  note =	 "NASA Conference Publication 10159",
  keywords = {epistemology, software},		  
  url = 	 {/~cmh/epsefm-tcabst.html}
}

@techreport{Butler-RCP-III,
  author = "Ricky W. Butler and Ben L. {Di Vito} and C. Michael Holloway",
  title = {{Formal Design and Verification of a Reliable Computing Platform
		  For Real-Time Control (Phase 3 Results)}}, 
  month = aug,  year = 1994,
  institution = larc,
  number = 109140,
  type = TM,
  keywords = {RCP, EHDM, design, proofs},		  
  postscript={ftp://air16.larc.nasa.gov/pub/fm/papers/1994/rcp-phase-III.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1718/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201718%20/usr/local/web/htdocs/ltrs/refer/1994/tm109140.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201718%20/usr/local/web/htdocs/ltrs/refer/1994/tm109140.refer.html;7=%00;},                 
}

@techreport{Butler-PVS-tutorial,
  title = {{An Elementary Tutorial on Formal Specification and 
  Verification Using PVS}},
  author = "Ricky W. Butler",
  month = sep, year = 1993,
  institution = larc,
  number = "108991",
  type = TM,
  note = {Revised in 1995},
  keywords = {PVS, tutorial, requirements, proofs},		  
  postscript={ftp://air16.larc.nasa.gov/pub/fm/papers/1995/revised-pvs-tutorial.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1843/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201843%20/usr/local/web/htdocs/ltrs/refer/1993/tm108991.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201843%20/usr/local/web/htdocs/ltrs/refer/1993/tm108991.refer.html;7=%00;},                
}

@inproceedings{Butler-FM-critical,
  author = "Ricky W. Butler and Sally C. Johnson",
  title = {{Formal Methods For Life-Critical Software}},
  booktitle = "Computing in Aerospace 9 Conference",
  year = 1993, month = oct, day = "19--21", pages = "319-329",
  address = "San Diego, California",
  keywords = {tutorial},		  
  url = {paper-cia/paper.html}	   
}

@techreport{Miner-clk-tp,
  author = "Paul S. Miner",
  title = {{Verification of Fault-Tolerant Clock Synchronization Systems}}, 
  month = nov,	year = 1993,
  institution = larc,
  number = 3349,
  keywords = {hardware, clock, EHDM, proofs},		  
  postscript = {ftp://techreports.larc.nasa.gov/pub/techreports/larc/93/tp3349.ps.Z},
  type = TP,
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2482/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202482%20/usr/local/web/htdocs/ltrs/refer/1993/rdp3349.tex.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202482%20/usr/local/web/htdocs/ltrs/refer/1993/rdp3349.tex.refer.html;7=%00;},                
}

@article{Butler-nonq-TSE,
  title = {{The Infeasibility of Quantifying the Reliability of Life-Critical
		  Real-Time Software}}, 
  author = "Ricky W. Butler and George B. Finelli",
  journal = ieeetse, volume = 19, number = 1,
  month = jan, year = 1993, pages = "3-12",
  keywords = {reid award},		  
  url = {paper-nonq/nonq-tse.html}
}

@inproceedings{DiVito-RTSS-1,
  author = "Ben L. {Di Vito} and Ricky W. Butler",
  title = {{Provable Transient Recovery for Frame-Based, Fault-Tolerant
		  Computing Systems}}, 
  month = dec, day = "2--4", year = 1992,
  booktitle = "Real-Time Systems Symposium",
  address = "Phoenix, Arizona",
  keywords = {RCP, EHDM, design, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/rtss-92.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1734/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201734%20/usr/local/web/htdocs/ltrs/refer/1992/rtss-92.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201734%20/usr/local/web/htdocs/ltrs/refer/1992/rtss-92.refer.html;7=%00;},                 
}

@techreport{Johnson-FM-wkshp-II,
  author = "Sally C. Johnson and C. Michael Holloway and Ricky W. Butler (editors)",
  title = {{Second NASA Formal Methods Workshop 1992}},
  month = nov, year = 1992,
  institution = larc,
  number = 10110,
  keywords = {workshop, technology transfer, proofs, design},		  
  type = CP
}

@inproceedings{Miner-clk-design,
  author = "Paul S. Miner and Peter A. Padilla and Wilfredo Torres",
  title = {{A Provably Correct Design of a Fault-Tolerant Clock
		  Synchronization Circuit}}, 
  month = oct, year = 1992, pages = "341-346",
  booktitle = "11th Digital Avionics Systems Conference", 
  keywords = {hardware, clock, EHDM, proofs},		  
  address = "Seattle, Washington"
}

@incollection{DiVito-formal-tech,
  author = "Ben L. {Di Vito} and Ricky W. Butler",
  title = {{Formal Techniques for Synchronized Fault-Tolerant Systems}},
  year = 1993,
  series = "Dependable Computing and Fault-Tolerant Systems",
  booktitle = "Dependable Computing for Critical Applications 3",
  publisher = "Springer Verlag",
  address = "New York",
  note = "Also presented at 3rd IFIP Working Conference on Dependable
		  Computing for Critical Applications, Mondello, Sicily,
		  Italy, Sept. 14--16, 1992",
  pages = "279--306",
  keywords = {RCP, EHDM, design, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/IFIP-92.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1780/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201780%20/usr/local/web/htdocs/ltrs/refer/1992/ifip-92.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201780%20/usr/local/web/htdocs/ltrs/refer/1992/ifip-92.refer.html;7=%00;},	           
}

@techreport{Miner-des-prelim-tm,
  author = "Paul S. Miner",
  title = {{A Verified Design of a Fault-Tolerant Clock Synchronization
		  Circuit: Preliminary Investigations}}, 
  month = mar,	year = 1992,
  institution = larc,
  number = 107568,
  keywords = {hardware, clock, EHDM, proofs},		  
  type = TM
}

@incollection{DiVito-os-IFIP,
  author = "Ben L. {Di Vito} and Ricky W. Butler and James L. Caldwell",
  title = {{High Level Design Proof of a Reliable Computing Platform}},
  year = 1992,
  series = "Dependable Computing and Fault-Tolerant Systems",
  booktitle = "Dependable Computing for Critical Applications 2",
  publisher = "Springer Verlag",
  address = "New York",
  note = "Also presented at 2nd IFIP Working Conference on Dependable 
          Computing for Critical Applications, Tucson, Arizona, 
          Feb. 18--20, 1991, pp. 124--136",
  pages = "279--306",
  keywords = {RCP. EHDM, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/rcp-IFIP.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/2016/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%202016%20/usr/local/web/htdocs/ltrs/refer/1991/rcp-ifip.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%202016%20/usr/local/web/htdocs/ltrs/refer/1991/rcp-ifip.refer.html;7=%00;},          
}

@techreport{Miner-extend-tm,
  author = "Paul S. Miner",
  title = {{An Extension to Schneider's General Paradigm for Fault-Tolerant
		  Clock Synchronization}}, 
  year = 1992,
  institution = larc,
  number = 107634,
  keywords = {hardware, clock, EHDM, design, proofs},		  
  type = TM
}

@article{Johnson-des-for-val,
  author = "Sally C. Johnson and Ricky W. Butler",
  title = {{Design For Validation}},
  journal = "IEEE Aerospace and Electronics Systems",
  note = "Also appeared in the AIAA/IEEE 10th Digital Avionics Systems
        Conference, Los Angeles, California, Oct. 7-11, 1991, pp. 487-492",
  year = 1992, month = jan, pages = "38-43",
  keywords = {design, software, hardware},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/des-for-val.ps}	  
}

@techreport{Butler-RCP,
  author = "Ricky W. Butler and Ben L. {Di Vito}",
  title = {{Formal Design and Verification of a Reliable Computing Platform
		  For Real-Time Control (Phase 2 Results)}},  
  month = jan,	year = 1992,
  institution = larc,
  number = 104196,
  type = TM,
  keywords = {RCP, EHDM, design, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/rcp-phase-II.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1762/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201762%20/usr/local/web/htdocs/ltrs/refer/1992/tm104196.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201762%20/usr/local/web/htdocs/ltrs/refer/1992/tm104196.refer.html;7=%00;},	          
}
		  
@inproceedings{Butler-nonq,
  title = {{The Infeasibility of Experimental Quantification of Life-Critical
		  Software Reliability}}, 
  author = "Ricky W. Butler and George B. Finelli",
  booktitle = "Proceedings of the ACM SIGSOFT '91 Conference on Software for
		  Critical Systems", 
  address = "New Orleans, Louisiana",
  month = dec, day ="4-6", year = 1991, pages = "66-76",
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/infeasibility.ps}	  
}

@techreport{Carreno-VIPER,
  author = "Victor A. Carre{\~{n}}o and Rob K. Angellatta",
  title = {{A Case Study for the Real-Time Experimental Evaluation of the
		  VIPER Microprocessor}}, 
  month = sep, year = 1991,
  institution = larc, number = 104098,
  keywords = {hardware, VIPER},		  
  type = TM
}

@inproceedings{Butler-NASA-program,
  author = "Ricky W. Butler",
  title = {{NASA Langley's Research Program in Formal Methods}},
  month = Jun, days = "25--27",
  year = 1991,
  booktitle = "6th Annual Conference on Computer Assurance (COMPASS 91)",
  keywords = {technology transfer, overview},		  
  address = "Gaithersburg, Maryland"
}

@inproceedings{Butler-os,
  author = "Ricky W. Butler and James L. Caldwell and Ben L. {Di Vito}",
  title = {{Design Strategy for a Formally Verified Reliable Computing
		  Platform}},  
  month = Jun, days = "25--27",	year = 1991,
  booktitle = "6th Annual Conference on Computer Assurance (COMPASS 91)",
  address = "Gaithersburg, Maryland",
  keywords = {RCP, EHDM, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/compass91-paper.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1700/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201700%20/usr/local/web/htdocs/ltrs/refer/1991/compass-91.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201700%20/usr/local/web/htdocs/ltrs/refer/1991/compass-91.refer.html;7=%00;},	           
}
		  
@article{Butler-circuit-verif,
  title = {{Formal Design Verification of Digital Circuitry}},
  author = "Ricky W. Butler and Jon A. Sjogren",
  year = 1991,
  journal = "Reliability Engineering and System Safety",
  volume = 32, number = "1 and 2", pages = "67-93",
  keywords = {hardware, design},		  
}
	
@techreport{Butler-wkshp,
  author = "Butler, (editor), Ricky W. ",
  title = {{NASA Formal Methods Workshop 1990}},
  month = nov, year = 1990,
  institution = larc,
  number = 10052,
  type = CP,
  keywords = {overview},		  
}

@techreport{DiVito-os-TM,
  author = "Ben L. {Di Vito} and Ricky W. Butler and Caldwell, II, James L.", 
  title = {{Formal Design and Verification of a Reliable Computing Platform
		  For Real-Time Control (Phase 1 Results)}}, 
  month = oct,	year = 1990,
  institution = larc,
  number = 102716,
  type = TM,
  keywords = {RCP, EHDM, design, proofs},		  
  postscript = {ftp://air16.larc.nasa.gov/pub/fm/papers/1992-and-earlier/rcp-phase-I.ps},
  url={http://wais-gw.larc.nasa.gov:81/techreports.larc.nasa.gov:210/ltrs_index/HTML/1626/1=techreports%3A210;2=/usr/local/web/waissrc/ltrs_index;3=0%201626%20/usr/local/web/htdocs/ltrs/refer/1990/NASA-90-tm102716.refer.html;4=techreports%3A210;5=/usr/local/web/waissrc/ltrs_index;6=0%201626%20/usr/local/web/htdocs/ltrs/refer/1990/NASA-90-tm102716.refer.html;7=%00;},	          
}

@techreport{Butler-RSRE,
  title = {{Hardware Proofs Using EHDM and the RSRE Verification Methodology}},
  author = "Ricky W. Butler and Jon A. Sjogren",
  month = dec, year = 1988,
  institution = larc,
  number = 100669,
  type = TM,
  keywords = {hardware, design, proofs, EHDM},		  
}