% This is the bibliographic database in bibtex format.
@string{SV = "Springer Verlag"}
@string{NH = "North Holland"}
@string{NASA = ""}
@string{FAA = "{FAA}"}
@string{JCSS = "Journal Of Computer And System Sciences"}
@string{CR = "{NASA} Contractor Report"}
@string{CP = "{NASA} Conference Publication"}
@string{TM = "{NASA} Technical Memorandum"}
@string{TP = "{NASA} Technical Paper"}
@string{CLI = "Computational Logic Inc."}
@string{CSDL = "Charles Stark Draper Lab., Inc."}
@string{SEN = "ACM SIGSOFT Software Engineering Notes"}
@string{acm = {Association for Computing Machinery}}
@string{acsac = { Aerospace Computer Security Applications Conference}}
@string{afips = {AFIPS Conference Proceedings}}
@string{agard = {NATO Advisory Group for Aerospace Research and Development
		(AGARD)}}
@string{aiaa = {American Institute of Aeronautics and Astronautics}}
@string{ams = {American Mathematical Society}}
@string{annals = {Annals of the History of Computing}}
@string{awst = {Aviation Week and Space Technology}}
@string{cade = { International Conference on Automated Deduction (CADE)}}
@string{cav = {Computer-Aided Verification}}
@string{cipher = {Cipher (Newsletter of the {IEEE} Technical Committee
		on Security and Privacy)}}
@string{cj = {Computer Journal}}
@string{csl = {Computer Science Laboratory, SRI International}}
@string{csli = {Center for the Study of Language and Information}}
@string{csfw = {Proceedings of the Computer Security Foundations Workshop}}
@string{cup = {Cambridge University Press}}
@string{dasc = {{AIAA/IEEE} Digital Avionics Systems Conference}}
@string{dcca = {IFIP Working Conference on Dependable Computing for
		Critical Applications}}
@string{dcs = { International Conference on Distributed Computing Systems}}
@string{dover = {Dover Publications, Inc.}}
@string{facs = {Formal Aspects of Computing}}
@string{focs = { Annual Symposium on Foundations of Computer Science}}
@string{ftcs = {Fault Tolerant Computing Symposium }}
@string{gtm = {Graduate Texts in Mathematics}}
@string{hpj = {Hewlett-Packard Journal}}
@string{icse = {International Conference on Software Engineering}}
@string{ieeeaes = {IEEE Aerospace and Electronic Systems Magazine}}
@string{ieeecs = {IEEE Computer Society}}
@string{ieeecsm = {IEEE Control Systems Magazine}}
@string{ieee = {The Institute of Electrical and Electronics Engineers}}
@string{ieeepds = {IEEE Transactions on Parallel and Distributed Systems}}
@string{ieeesmc = {IEEE Transactions on Systems, Man and Cybernetics}}
@string{ieeetc = {IEEE Transactions on Computers}}
@string{ieeetr = {IEEE Transactions on Reliability}}
@string{ieeetse = {IEEE Transactions on Software Engineering}}
@string{ieepe = {IEE Proceedings, Part E: Computers and Digital Techniques}}
@string{ieepg = {IEE Proceedings, Part G: Circuits Devices and Systems}}
@string{ieepd = {IEE Proceedings, Part D: Control Theory and Applications}}
@string{Ipl = "Information Processing Letters"}
@string{Jacm = "Journal Of The {ACM}"}
@string{jar = {Journal of Automated Reasoning}}
@string{jsl = {Journal of Symbolic Logic}}
@string{jgcd = {AIAA Journal of Guidance, Control, and Dynamics}}
@string{larc = {NASA Langley Research Center}}
@string{lics = {Annual IEEE Symposium on Logic in Computer Science}}
@string{lnai = {Lecture Notes in Artificial Intelligence}}
@string{lncs = {Lecture Notes in Computer Science}}
@string{lnm = {Lecture Notes in Mathematics}}
@string{mp = {Menlo Park, CA}}
@string{naecon = {National Aerospace and Electronics Conference (NAECON)}}
@string{ncc = {National Computer Conference}}
@string{nist = {National Institute of Standards and Technology}}
@string{ny = {New York, NY}}
@string{oup = {Oxford University Press}}
@string{phiscs = {Prentice Hall International Series in Computer Science}}
@string{podc = { ACM Symposium on Principles of Distributed Computing}}
@string{popl = { ACM Symposium on Principles of Programming Languages}}
@string{rts = {Real-Time Systems}}
@string{rtss = {Real Time Systems Symposium}}
@string{scp = {Science of Computer Programming}}
@string{sen = {ACM Software Engineering Notes}}
@string{sosp = { ACM Symposium on Operating System Principles}}
@string{spe = {Software---Practice and Experience}}
@string{srds = { Symposium on Reliable Distributed Systems}}
@string{srsp = {Proceedings of the Symposium on Research in Security
		and Privacy}}
@string{ssp = {Proceedings of the Symposium on Security and Privacy}}
@string{sv = {Springer Verlag}}
@string{svwc = {Springer-Verlag Workshops in Computing}}
@string{tcs = {Theoretical Computer Science}}
@string{toplas = {ACM Transactions on Programming Languages and Systems}}
@string{tosem = {ACM Transactions on Software Engineering and Methodology}}
@string{wiley = {John Wiley and Sons}}

@MANUAL{fm-guidebook-1-1,
	KEY = {NAS},
	ORGANIZATION = {NASA
              Office of Safety and Mission Assurance},
	TITLE = {Formal Methods Specification and Verification
              Guidebook for Software and Computer Systems,
              Volume I: Planning and Technology Insertion},
        MONTH = jul,
	YEAR = 1995,
        NOTE = {NASA-GB-002-95, Release 1.0.},
	ADDRESS = {Washington, DC}
}

@MANUAL{fm-guidebook-2-1,
	KEY = {NAS},
	ORGANIZATION = {NASA
              Office of Safety and Mission Assurance},
	TITLE = {Formal Methods Specification and Analysis
              Guidebook for the Verification of Software
	      and Computer Systems,
              Volume II: A Practitioner's Companion},
	ADDRESS = {Washington, DC},
        MONTH = may,
	YEAR = 1997,
        NOTE = {NASA-GB-001-97, Release 1.0. Available
                at {\tt http://eis.jpl.nasa.gov/quality/Formal\_Methods/}.}
}

@MANUAL{safer-rqmts,
	KEY = {NAS},
	TITLE = {Project Requirements Document for the
		  Simplified Aid for EVA Rescue (SAFER) Flight Test Project},
        note = {NASA JSC-24691},
	MONTH = dec,
	YEAR = 1992
}

@MANUAL{safer-ops-manual,
	KEY = {NAS},
	TITLE = {Simplified Aid for EVA Rescue (SAFER), Operations Manual},
        note = {NASA JSC-26283},
	MONTH = sep,
	YEAR = 1994
}

@MANUAL{safer-spec,
	KEY = {NAS},
	TITLE = {Simplified Aid for EVA Rescue (SAFER) Flight Test Project
		  - Flight Test Article Prime Item Development 
		  Specification},
        note = {NASA JSC-25552},
	MONTH = jul,
	YEAR = 1994
}
		  		  
@article{Owre-prolegomena,
	AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar and 
                  Friedrich von Henke},
	TITLE = {Formal Verification for Fault-Tolerant Architectures:
                 Prolegomena to the Design of {PVS}},
	JOURNAL = ieeetse,
	YEAR = 1995, MONTH = feb, volume = 21, number = 2,
        pages = "107-125"
}
        
@inproceedings{Butler-Compass95,
	author = "Ricky W. Butler and James L. Caldwell and
                  Victor A. Carreno and C. Michael Holloway and Paul S. Miner 
                  and Ben L. Di Vito",
	title = "{NASA} {L}angley'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"}

@techreport{Rushby-FAA,
	title = "Formal Methods and Digital Systems Validation for Airborne 
                 Systems",
        author = "John Rushby",
	year = 1993, month = dec,
	number = 4551,
        type = CR}

@techreport{Rushby-FAA-short,
	title = "Formal Methods and Their Role in Digital Systems 
                 Validation for Airborne Systems",
        author = "John Rushby",
	year = 1995, month = aug,
	number = 4673,
	institution = NASA,
        type = CR}
		  		  
@article{Crow-DiVito98,
	AUTHOR = {Judith Crow and Ben Di Vito},
	TITLE = {Formalizing {Space Shuttle} Software Requirements:
                 Four Case Studies},
	JOURNAL = tosem,
	YEAR = 1998, MONTH = jul, volume = 7, number = 3,
        pages = {296-332}
}
		  		  
@article{Srivas-Miller96,
	AUTHOR = {M.~K. Srivas and S.~P. Miller},
	TITLE = {Applying Formal Verification to the {AAMP5} Microprocessor:
                 A Case Study in the Industrial Use of Formal Methods},
	JOURNAL = {Formal Methods in Systems Design},
	YEAR = 1996, MONTH = mar, volume = 8, number = 2,
        pages = {153-188}
}
        
@inproceedings{Agerholm-Larsen97,
	author = "Sten Agerholm and Peter Gorm Larsen",
	title = "Modeling and Validating {SAFER} in {VDM-SL}",
        month = sep, days = "10--12",
	year = 1997,
        booktitle = "Lfm97, Fourth {NASA Langley} Formal Methods Workshop",
	address = "Hampton, Virgina",
        note = "{NASA Conference Publication} 3356." }

@book{Gordon-Melham93,
      title = {Introduction to HOL: A Theorem Proving Environment
               for Higher-Order Logic},
      author = {M.~J.~C. Gordon and T.~F. Melham},
      publisher = {Cambridge University Press},
      address = {Cambridge, England},
      year = 1993
}

@book{Paulson87,
      title = {Logic and Computation: Interactive Proof with
               Cambridge LCF},
      author = {L.~C. Paulson},
      publisher = {Cambridge University Press},
      address = {Cambridge, England},
      year = 1987
}
		  		  
@article{Harel+90,
	AUTHOR = {D. Harel and H. Lachover and A. Naamad and
                  A. Pnueli and M. Politi and R. Sherman and
                  A. Shtull-Trauring and M. Trakhtenbrot},
	TITLE = {Statemate: A Working Environment for the Development
                 of Complex Reactive Systems},
	JOURNAL = ieeetse,
	YEAR = 1990, MONTH = apr, volume = 16, number = 4,
        pages = "403-414"
}
		  		  
@article{Heitmeyer+96,
	AUTHOR = {C. L. Heitmeyer and R. D. Jeffords and B. L. Labaw},
	TITLE = {Consistency Checking of {SCR}-Style Requirements
                 Specifications},
	JOURNAL = tosem,
	YEAR = 1996, MONTH = jul, volume = 5, number = 3,
        pages = "231-261"
}
		  		  
@article{Leveson+94,
	AUTHOR = {N. G. Leveson and M. P. E. Heimdahl and H. Hildreth
                  and J. D. Reese},
	TITLE = {Requirements Specification for Process-Control Systems},
	JOURNAL = ieeetse,
	YEAR = 1994, MONTH = sep, volume = 20, number = 9,
        pages = "694-707"
}
		  		  
@article{Henzinger+97,
	AUTHOR = {Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi},
	TITLE = {{\sc HyTech:} A Model Checker for Hybrid Systems},
	JOURNAL = {Software Tools for Technology Transfer},
	YEAR = 1997, MONTH = dec, volume = 1, number = 1,
        pages = "110-122"
}