% This is Debbie's verification bibliography
%
% Last changed 04.03.93 changed ``'' to {}
%
% ----- A -----

@InProceedings{Aagaard92,
  author = 	{Mark Aagaard and Miriam Leeser},
  title = 	{Verifying a {L}ogic {S}ynthesis {T}ool in {N}uprl: A {C}ase {S}tudy in
		 {S}oftware {V}erification},
  booktitle = 	{Proceedings of the 4th Workshop on 
                 Computer Aided Verification},
  year = 	{1992},
  annote = 	{They verified a higher order
		 logic specification of a logic synthesis tool using Nuprl. It
		 was also  
		 implemented in Standard ML using corresponding definitions.
		 In some cases the definitions required by Nuprl were in a
		 different form to that required by  Standard ML.  Theorems
		 corresponding to the Standard ML style definitions were then
		 proved from the Nuprl definitions. }
}

% ----- B -----
@techreport{BevierKIT,
     AUTHOR      = {William R. Bevier},
     TITLE       = {A Verified Operating Systems Kernel},
     INSTITUTION = {CLInc},
     YEAR        = {1987},
     NUMBER      = {11},
     ANNOTE      = {}
     }

@techreport{Billstuff,
     AUTHOR      = {William R. Bevier},
     TITLE       = {The Formal Specification and Definition of {KIT}},
     INSTITUTION = {CLInc\footnote{Computational Logic, Inc., 
                    1717 W. Sixth St. Suite 290, Austin, TX 78703-4776}},
     YEAR        = {1987},
     NUMBER      = {16},
     ANNOTE      = {}
     }

@techreport{KIT,
     AUTHOR      = {William R. Bevier},
     TITLE       = {{KIT}: A {S}tudy in {O}perating {S}ystem {V}erification},
     INSTITUTION = {CLInc},
     YEAR        = {1988},
     NUMBER      = {28},
     ANNOTE      = {}
    }

@article{ShortKIT,
     AUTHOR  = {William R. Bevier},
     TITLE   = {Kit and the Short Stack},
     JOURNAL = {Journal of Automated Reasoning},
     YEAR    = {1989},
     VOLUME  = {5},
     NUMBER  = {4},
     MONTH   = {Dec},
     ANNOTE  = {}
     }

@InProceedings{Bevier87,
  author = 	{William R. Bevier and Warren A. Hunt, Jr. and William D.
		 Young}, 
  title = 	{Towards Verified Execution Environments},
  booktitle = 	{Proceedings of the 1987 {IEEE} Symposium on Security and
		 Privacy}, 
  year = 	{1987},
  pages = 	{106-115},
  month = 	{April}
}

@article{Approach,
     AUTHOR  = {William R. Bevier and Warren A. {Hunt, Jr.} 
                and {J Strother} Moore and William D. Young},
     TITLE   = {An {A}pproach to {S}ystems {V}erification},
     JOURNAL = {Journal of Automated Reasoning},
     YEAR    = {1989},
     VOLUME  = {5},
     NUMBER  = {4},
     MONTH   = {Dec},
     NOTE    = {also available as CLInc Technical Report 41, 1989}
     }

@BOOK{Bicarregui&93,
  KEY           = {Bicarregui\&93},
  AUTHOR        = {Juan Bicarregui, John Fitzgerald, Peter Lindsay,
                  Richard Moore and Brian Ritchie},
  TITLE         = {Proof in VDM: A Practitioner's Guide},
  PUBLISHER     = {Springer-Verlag},
  YEAR          = {1993},
  SIZE          = {245},
  NOTE          = {To appear},
  ANNOTE        = {},
  COMMENT       = {suggested by Peter Gorm Larson).}
  }

@book{DeduSys,
     AUTHOR    = {K.-H. Bl\"asius and H.-J. B\"urckert},
     TITLE     = {Deduktionssysteme : Automatisierung des logischen Denkens},
     PUBLISHER = {Oldenbourg},
     ADDRESS   = {M\"unchen},
     YEAR      = {1987},
     ANNOTE    = {}
     }

@ARTICLE{BPS:92,
        AUTHOR             = {Borrione, D. and Pierre, L. and Salem, A.},
        JOURNAL            = {{IEEE} Design and Test Magazine},
        TITLE              = {Formal Verification of {VHDL} Descriptions 
                              in the {PREVAIL} Environment},
        VOLUME             = {9},
        NUMBER             = {2},
        YEAR               = {1992}
}


@article{Bowen90,
	author  = {Jonathan Bowen},
	title   = {Formal Specification of the {ProCoS/safemos} 
                   Instruction Set},
	journal = {Microprocessors and Microsystems},
	volume  = 14,
	number  = 10,
	year    = 1990,
	month   = {December},
	pages   = {631 -- 643}
        }

@book{BlackBook,
     AUTHOR    = {Robert S. Boyer and {J Strother} Moore},
     TITLE     = {A Computational Logic},
     PUBLISHER = {Academic Press},
     ADDRESS   = {New York},
     YEAR      = {1979},
     ANNOTE    = {}
     }

@book{PurpleBook,
     AUTHOR    = {Robert S. Boyer and {J Strother} Moore},
     TITLE     = {A Computational Logic Handbook},
     PUBLISHER = {Academic Press},
     ADDRESS   = {New York},
     YEAR      = {1988},
     ANNOTE    = {}
     }

@article{RSA,
     AUTHOR    = {Robert S. Boyer and {J Strother} Moore},
     TITLE     = {Proof Checking the RSA Public Key Encryption
		  Algorithm},
     JOURNAL   = {American Mathematical Monthly},
     VOLUME    = {91},
     NUMBER    = {3},
     YEAR      = {1984},
     PAGES     = {133-167}
     }


@article{Unsolvability,
     AUTHOR    = {Robert S. Boyer and {J Strother} Moore},
     TITLE     = {A Mechanical Proof of the Unsolvability of the 
                  Halting Problem},
     JOURNAL   = {Journal of the ACM},
     VOLUME    = {31},
     NUMBER    = {3},
     MONTH     = {July},
     YEAR      = {1984},
     PAGES     = {441-458}
     }      

@InProceedings{Boyer92,
  author    = {Robert S. Boyer and Yuan Yu},
  title     = {Automated Proofs of Object Code for a Widely Used 
               Microprocessor},
  booktitle = {Proceedings of the 11th International Conference on
               Automated Deduction},
  year      = {1992}
  }



@techreport{VIPER,
     AUTHOR      = {Bishop Brock and Warren A. {Hunt, Jr.}},
     TITLE       = {Report on the Formal Specification and Partial Verification of
                    the {VIPER} Microprocessor},
     INSTITUTION = {CLInc},
     YEAR        = {1989},
     NUMBER      = {46},
     ANNOTE      = {}
     }

@phdthesis{Bronstein,
     AUTHOR      = {A. Bronstein},
     TITLE       = {MLP: String-functional semantics and {B}oyer-{M}oore
	            mechanization for the formal verification of
		    synchronous circuits},
     SCHOOL      = {Stanford University},
     YEAR        = {1989}
     }

@book{Biundo,
     AUTHOR      = {Susanne Biundo},
     TITLE       = {Automatische Synthese rekursiver Programme als Beweisverfahren},
     PUBLISHER   = {Springer Verlag},
     ADDRESSE    = {Berlin},
     YEAR        = {1992},
     ANNOTE      = {Susanne's PhD}
     }

@inproceedings{INKA,
     AUTHOR      = {S. Biundo and B. Hummel and D. Hutter and C. Walther},
     TITLE       = {The {K}arlsruhe Induction Theorem Proving System},
     BOOKTITLE   = {Proceedings 8th CADE},
     SERIES      = {LNCS 230},
     YEAR        = {1986},
     ANNOTE      = {}
     }

@techreport{AddAssign,
     AUTHOR      = {Bettina Buth and Karl-Heinz Buth and 
                    Ursula Martin and Victoria Stavridou},
     TITLE       = {Experiments with Program Verification Systems},
     INSTITUTION = {ProCoS\footnote{ProCos reports reflect work which
                   was partially funded by the Commission of the European Communities (CEC) under the
                   ESPRIT programme in the field of Basic Research Action
                   project no.\ 3104: ``ProCoS: Provably Correct Systems'' and are
                   available from the authors or from
                   Dines Bj\o rner, Department of Computer Science, Technical University of Denmark,
                   Building 344\O, DK-2800 Lyngby, Denmark}},
     ADDRESS     = {Kiel, London},
     YEAR        = {1989},
     NUMBER      = {BB 2},
     ANNOTE      = {}
     } 

@InProceedings{Buth92,
  author = 	{Bettina Buth and K. H. Buth and M. Fraenzle and B. V. Karger
		 and Y. Lakhneche and K. Langmaack and M. Mueller-Olm},
  title = 	{Provably Correct Compiler Development and Implementation},
  booktitle = 	{Compiler Construction '92},
  year = 	{1992},
  pages = 	{141-155},
  publisher = 	{Springer-Verlag},
  volume = 	{641},
  series = 	{LNCS}
}


@techreport{KHB3,
     AUTHOR      = {Karl-Heinz Buth
 and Debora Weber-Wulff},
     TITLE       = {The ``{A}utomated {P}roving and {T}erm {R}ewriting'' {P}raktikum},
     INSTITUTION = {ProCoS},
     ADDRESS     = {Kiel},
     MONTH       = {February},
     YEAR        = {1991},
     NUMBER      = {KHB 3}
     }

% ----- C -----

@PhdThesis{Camilleri88,
  author = {Albert John Camilleri},
  title  = {Executing Behavioural Definitions in Higher Order Logic},
  school = {University of Cambridge, Computer Laboratory},
  year   = {1988},
  month  = {Feb}
}

@TechReport{CamilleriJ91a,
  author      = {Juanito Camilleri},
  title       = {Symbolic Compilation and Execution of Programs by Proof: A
		 Case study in {HOL}},
  institution = {University of Cambridge, Computer Laboratory},
  year        = {1991},
  number      = {240},
  month       = {December}
}

@TechReport{Cardell-Oliver90,
  author      = {Rachel Cardell-Oliver},
  title       = {Formal Verification of Real Time Protocols using Higher Order
		 Logic}, 
  institution = {University of Cambridge, Computer Laboratory},
  year        = {1990},
  number      = {206},
  month       = {August}
}

@techreport{AnnotatedGypsy,
     AUTHOR      = {Miren Carranza and William D. Young},
     TITLE       = {An Annotated {G}ypsy Bibliography},
     INSTITUTION = {CLInc Internal Note},
     YEAR        = {1989},
     NUMBER      = {105},
     ANNOTE      = {}
     }                  

 @InProceedings{Carter78,
   author = 	{William C. Carter and  William H. Joyner, Jr.
                 and  Daniel Brand},
   title = 	{Microprogram Verification Considered Necessary},
   booktitle = 	{{AFIPS} Conference Proceedings 1978 National Computer Conference},
   year = 	{1978},
   editor = 	{Saki P. Ghosh and Leonard Y. Liu},
   pages = 	{657-664},
   publisher = 	{{AFIPS} Press},
   volume = 	{47},
   month = 	{June}
 }


@book{ChangLee,
     AUTHOR    = {C. Chang and R. Lee},
     TITLE     = {Symbolic Logic and Mechanical Theorem Provers},
     PUBLISHER = {Academic Press},
     ADDRESS   = {New York},
     YEAR      = {1973},
     ANNOTE    = {}
     }

@Article{Chirica86,
  author = 	"Laurian M. Chirica and David F. Martin",
  title = 	"Towards Compiler Implementation Correctness Proofs",
  journal = 	"{ACM} Transactions on Programming Languages and Systems",
  year = 	"1986",
  volume = 	"8",
  number = 	"2",
  pages = 	"185-214",
  month = 	"April"
}

 @Article{Clutterbuck88,
   author = 	"D. L. Clutterbuck and B. A. Carr\'{e}",
   title = 	"The Verification of Low Level Code",
   journal = 	"Software Engineering Journal",
   year = 	"1988",
   pages = 	"97-111",
   month = 	"May"
 }


@techreport{ProvingGypsy,
     AUTHOR      = {Richard M. Cohen},
     TITLE       = {Proving {G}ypsy Programs},
     INSTITUTION = {CLInc Technical Report},
     ADDRESS     = {Austin, Texas},
     YEAR        = {1989},
     NUMBER      = {4b},
     ANNOTE      = {}
     }

@InCollection{Cohn87,
  author = 	"Avra Cohn",
  title = 	"A Proof of Correctness of the {V}iper Microprocessor: The
		 First  Level",
  booktitle = 	"{VLSI} Specification, Verification and Synthesis",
  publisher = 	"Kluwer Academic Publishers",
  year = 	"1988",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  chapter = 	"1",
  pages = 	"1--91"
}

@InCollection{Cohn88,
  author = 	"Avra Cohn",
  title = 	"Correctness Properties of the {V}iper Block Model: The
		 Second  Level",
  booktitle = 	"Current Trends in Hardware Verification and Automated
		 Theorem Proving",
  publisher = 	"Springer-Verlag",
  year = 	"1989",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  chapter = 	"2",
  pages = 	"27--72"

}

@Article{Cohn89,
  author = 	"Avra Cohn",
  title = 	"The notion of proof in hardware verification",
  journal = 	"Journal of Automated Reasoning 5",
  year = 	"1989",
  number = 	"5",
  pages = 	"127-138"
}

@techreport{CohnMilner,
     AUTHOR      = {Avra Cohn and Robin Milner},
     TITLE       = {On using {E}dinburgh {LCF} to prove the correctness
                    of a parsing algorithm},
     INSTITUTION = {University of Edinburgh},
     YEAR        = {1982},
     NUMBER      = {CSR-112-82}
     }

@techreport{CohnParsing,
     AUTHOR      = {Avra Cohn},
     TITLE       = {The Correctness of a Precedence Parsing Algorithm in {LCF}},
     INSTITUTION = {University of Cambridge},
     YEAR        = {1982},
     MONTH       = {April},
     NUMBER      = {21}
     }


@Article{Collier86,
  author = 	"P. A. Collier",
  title = 	"Simple Compiler Correctness -- A Tutorial on the
                 Algebraic Approach",
  journal = 	"The Australian Computer Journal",
  year = 	"1986",
  volume = 	"18",
  number = 	"3",
  month = 	"August"
}

@book{Nuprl,
     KEY       = {Constable 1986},
     AUTHOR    = {{R. L.} {Constable, et al}},
     TITLE     = {Implementing mathematics with the {N}uprl proof development system},
     PUBLISHER = {Prentice Hall},
     ADDRESS   = {Englewood Cliffs, NJ},
     YEAR      = {1986},
     ANNOTE    = {}
     }

@inproceedings{DanFME,
     AUTHOR    = {Dan Craigen and Susan Gerhart and Ted Ralston},
     TITLE     = {Formal Methods Reality Check: Industrial Usage},
     BOOKTITLE = {{FME}'93 Symposium: Industrial Strength Formal Methods. Odense, Denmark.},
     YEAR      = {1993},
     PAGES     = {to appear},
     ANNOTE    = {}
    }	
{Cullyer85,
  author = 	"W. J. Cullyer",
  title = 	"{V}iper Processor; Formal Specification",
  institution = 	"{R}oyal {S}ignals and {R}adar {E}stablishment, {M}alvern",
  year = 	"1985"
}

@InCollection{Cullyer88,
   author = 	"W. J. Cullyer",
   title = 	"Implementing Safety Critical Systems: The {V}iper
		  {M}icroprocessor ",
   booktitle = 	"{VLSI} Specification, Verification and Synthesis",
   publisher = 	"Kluwer Academic Publishers",
   year = 	"1988",
   pages = 	"1--25",
   editor = 	"G. Birtwistle and P. A. Subrahmanyam"
}

@TechReport{Curzon91THESIS,
  author = 	"Paul Curzon",
  title = 	"A Structured Approach to the Verification of Low Level Microcode",
  institution = 	"University of Cambridge",
  year = 	"1991",
  number = 	"215",
  month = 	feb,
}

@InProceedings{Curzon91,
  author = 	"Paul Curzon",
  title = 	"A Verified Compiler for a Structured Assembly Language",
  booktitle = 	"Proceedings of the 1991 International Workshop on the {HOL}
		 Theorem Proving System and its Applications",
  year = 	"1992",
  editor = 	"Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and
                 Phillip J. Windley",
  publisher = 	"{IEEE} Computer Society Press",
}

@InProceedings{Curzon92DCCA,
  key = "Curzon92b",
  author = 	"Paul Curzon",
  title = 	"Compiler Correctness and Input/Output",
  booktitle = 	"Proceedings of the 3rd {IFIP} Working Conference on
		 Dependable Computing for Critical Applications",
  year = 	"1992",
  publisher = 	"Springer-Verlag",
  series = 	"Dependable Computing and Fault-Tolerant Computing",
  note = 	"To be published."
}


@InProceedings{Curzon92LPAR,
  key = "Curzon92a",
  author = 	"Paul Curzon",
  title = 	"A Programming Logic For a Verified Structured Assembly Language",
  booktitle = 	"Logic Programming and Automated Reasoning",
  year = 	"1992",
  editor = 	"A. Voronkov",
  pages = 	"403-408",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  volume = 	"624",
  series = 	"Lecture Notes in Artificial Intelligence"
}

@InProceedings{Curzon92HOL,
  author = 	"Paul Curzon",
  title = 	"Deriving Correctness Properties of Compiled Code",
  booktitle = 	"International Workshop on Higher
                 Order Logic Theorem Proving and its Applications",
  year = 	"1992",
  editor = 	"L. Claesen and M. Gordon"
}

% ----- D -----

@article{DeMillo,
     AUTHOR  = {R. De{M}illo and R. Lipton and A. Perlis},
     TITLE   = {Social processes and proofs of theorems and programs},
     JOURNAL = {CACM},
     YEAR    = {1979},
     VOLUME  = {22},
     NUMBER  = {5},
     MONTH   = {May},
     PAGES   = {271-280},
     ANNOTE  = {}
     }

@InProceedings{Despeyroux86,
  author = 	"Jo{\"e}lle Despeyroux",
  title = 	"Proof of Translation in Natural Semantics",
  booktitle = 	"{IEEE} symposium on Logic in Computer Science",
  year = 	"1986",
  pages = 	"193-205",
  OPTmonth = 	"June"
}

% ----- F -----

@article{Fetzer,
     AUTHOR  = {James H. Fetzer},
     TITLE   = {Program verification: {T}he very idea},
     JOURNAL = {CACM},
     YEAR    = {1988},
     VOLUME  = {31},
     NUMBER  = {9},
     MONTH   = {September},
     PAGES   = {1048-1063},
     ANNOTE  = {The begin of the Fetzer-fight}
     }


 @InProceedings{Floyd67,
   author = 	"Robert W. Floyd",
   title = 	"Assigning Meanings to Programs",
   booktitle = 	"Proceedings of the Symposium on Applied Mathematics",
   year = 	"1967",
   pages = 	"19-32",
   volume = 	"19"
 }


% ----- G -----


@TechReport{Glindtvad91,
  author = 	"Karin Glingtvad and Hanne Riis Nielson",
  title = 	"Correctness Preserving Transformations on a Multipass Occam
		 Compiler",
  institution = 	"Computer Science Department, Aarhus University",
  year = 	"1991",
  number = 	"DAIMI PB-368",
  month = 	oct
}

@inproceedings{Gloess,
     AUTHOR      = {Paul Gloess},
     TITLE       = {An Experiment with the {B}oyer-{M}oore Theorem Prover:
                    A proof of the correctness of a simple parser of
                    expressions},
     BOOKTITLE   = {LNCS 87 : Proceedings of the CADE-5},
     PAGES       = {154-169},
     YEAR        = {1980},
     PUBLISHER   = {Springer Verlag},
     ADDRESS     = {Berlin}
     }

@Article{Gomard91,
  author = 	"Carsten K. Gomard and Neil D. Jones",
  title = 	"A Partial Evaluator for the Untyped Lambda Calculus",
  journal = 	"Journal of Functional Programming",
  year = 	"1991",
  volume = 	"1",
  number = 	"1",
  pages = 	"21-69"
}

@techreport{good90,
	Key      = "Good",
	Author   = "Donald I. Good, Ann E. Siebert, William D. Young",
	Title    = "Middle Gypsy 2.05 Definition",
                    Institution="Computational Logic, Inc.",
	Number   = "CLI-59",
        Month    = "June",
        Year     = "1990"
       }

@techreport{GypsyMethod,
     AUTHOR      = {Donald I. Good and Benedetto L. DiVito and Michael K. Smith},
     TITLE       = {Using the {G}ypsy Methodology},
     INSTITUTION = {CLInc},
     YEAR        = {1988},
     NUMBER      = {2b},
     NOTE        = {Classified}
     }

@techreport{GypsyReport,
     AUTHOR      = {Donald I. Good and Robert L. Akers and Lawrence M. Smith},
     TITLE       = {Report on {G}ypsy 2.05},
     INSTITUTION = {CLInc},
     YEAR        = {1989},
     NUMBER      = {1c},
     NOTE        = {Classified}
     }  

@techreport{HOL,
     AUTHOR      = {{Michael J. C.} Gordon},
     TITLE       = {{HOL}: a machine oriented formulation of higher order logic},
     INSTITUTION = {University of Cambridge Computer Laboratory},
     YEAR        = {1985},
     NUMBER      = {68},
     ANNOTE      = {}
     }

@Book{Gordon79a,
  author = 	"Michael J. C. Gordon",
  title = 	"The denotational description of programming languages: an
		 introduction", 
  publisher = 	"Springer-Verlag",
  year = 	"1979"
}

@InCollection{Gordon87,
  author = 	"{Michael J. C.} Gordon",
  title = 	"{HOL}: A proof Generating System for Higher Order Logic",
  booktitle = 	"{VLSI} Specification, Verification and Synthesis",
  publisher = 	"Kluwer Academic Publishers",
  year = 	"1988",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  chapter = 	"3",
  pages = 	"73--128"

}

@book{EdinburghLCF,
      AUTHOR      = {Michael Gordon and Robin Milner and Christopher Wadsworth},
      TITLE       = {Edinburgh LCF},
      PUBLISHER   = {Springer Verlag},
      ADDRESS     = {New York},
      YEAR        = {1979}
      }


@InCollection{Gordon88,
  author = 	"Michael J. C. Gordon",
  title = 	"Mechanizing Programming Logics in Higher Order Logic",
  booktitle = 	"Current Trends in Hardware Verification and Automated
		 Theorem Proving",
  publisher = 	"Springer-Verlag",
  year = 	"1989",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  OPTchapter = 	"10",
  pages = 	"387--439"
}

@InProceedings{Gordon91,
  author = 	"Michael J. C. Gordon",
  title = 	"A Formal Method for Hard Real-Time Programming",
  booktitle = 	"4th Refinement Workshop",
  year = 	"1991",
  editor = 	"Joseph M. Morris and Roger C. Shaw",
  pages = 	"378-410",
  organization = 	"BCS-FACS",
  publisher = 	"Springer-Verlag",
  series = 	"Workshops In Computing",
  month = 	jan
}


% ----- H -----


@InProceedings{Hale91,
  author = 	"Roger Hale",
  title = 	"Reasoning about Software",
  booktitle = 	"Proceedings of the 1991 International Workshop on the {HOL}
		 Theorem Proving System and its Applications (Tutorial)",
  year = 	"1992",
  OPTeditor = 	"Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and
                 Phillip J. Windley",
  pages = 	"52-58",
  publisher = 	"{IEEE} Computer Society Press"
}

@Article{Hamel92,
  author = 	"Lutz H. Hamel",
  title = 	"Industrial Strength Compiler Construction with Equations",
  journal = 	"{ACM} {SIGPLAN} Notices",
  year = 	"1992",
  volume = 	"27",
  number = 	"8",
  pages = 	"43-50",
  month = 	"August",
  note = 	""
}

@Article{Hatcher91,
  author = 	"P. J. Hatcher",
  title = 	"The equational Specification of efficient compiler
                 code generation",
  journal = 	"Computer Languages",
  year = 	"1991",
  volume = 	"16",
  number = 	"1",
  pages = 	"81-95"
}


@Article{Hehner90,
  author = 	"Eric C. R. Hehner",
  title = 	"A practical theory of programming",
  journal = 	"Science of Computer Programming",
  year = 	"1990",
  number = 	"14",
  pages = 	"133-158"
}


@incollection{KIV,
     AUTHOR    = {M. Heisel and W. Menzel and W. Reif and W. Stephan},
     BOOKTITLE     = {Sichere {S}oftware. Formale {S}pezifikation und
                 {V}erifikation vertrauensw\"urdiger {S}ysteme},
     EDITOR    = {Heinrich Kersten},
     TITLE   = {Der {K}arlsruhe {I}nteractive {V}erifier ({KIV})},
     PAGES     = {172-193},
     PUBLISHER = {H\"uthig Buch Verlag},
     ADDRESS   = {Heidelberg},
     YEAR      = {1990},
     ANNOTE    = {}
    }
     

@Article{Hoare73,
  author = 	"C. A. R. Hoare and N. Wirth",
  title = 	"An axiomatic definition of the programming language {PASCAL}",
  journal = 	"Acta Informatica",
  year = 	"1973",
  volume = 	"2",
  pages = 	"335-355"
 }

@Article{Hoare69,
  author = 	"C. A. R. Hoare",
  title = 	"An Axiomatic Basis for Computer Programming",
  journal = 	"Communications of the {ACM}",
  year = 	"1969",
  volume = 	"12",
  number = 	"10",
  pages = 	"576-580,583",
  month = 	oct
}


@Book{Hoare85,
  author = 	"C. A. R. Hoare",
  title = 	"Communicating Sequential Processes",
  publisher = 	"Prentice Hall International",
  year = 	"1985"
}


@techreport{HuntFM8501,
     AUTHOR  = {Warren A. {Hunt, Jr.}},
     TITLE   = {The Mechanical Verification of a Microprocessor Design},    
     INSTITUTION = {CLInc},
     YEAR        = {1987},
     NUMBER      = {6},
     ANNOTE      = {}
     }




@article{HuntMDV,
     AUTHOR  = {Warren A. {Hunt, Jr.}},
     TITLE   = {Microprocessor Design Verification},
     JOURNAL = {Journal of Automated Reasoning},
     YEAR    = {1989},
     VOLUME  = {5},
     NUMBER  = {4},
     MONTH   = {Dec},
     NOTE    = {also  available as CLInc Technical Report 48, 1989}
     }

@article{WrongVerification,
     AUTHOR  = {Wim Hesselink and Jan Jongejan},
     TITLE   = {Duplicate Deletion Derived},
     JOURNAL = {CACM},
     YEAR    = {1992},
     VOLUME  = {35},
     NUMBER  = {7},
     MONTH   = {July},
     PAGES   = {99-107},
     ANNOTE  = {Derivation of BagsToSet, but with error and rejoinder}
     }

% ----- J -----

@TechReport{Joyce86,
  author = 	"Jeff Joyce and Graham Birtwistle and Mike Gordon",
  title = 	"Proving a Computer Correct in Higher Order Logic",
  institution = 	"University of Cambridge, Computer Laboratory",
  year = 	"1986",
  number = 	"100",
  month = 	dec
}


@InProceedings{Joyce89b,
  author = 	"Jeffrey J. Joyce",
  title = 	"Totally Verified Systems: Linking Verified Software to
		 Verified Hardware",
  booktitle = 	"Specification, Verification and Synthesis: Mathematical
		 Aspects",
  year = 	"1989",
  editor = 	"M. Leeser and G. Brown",
  publisher = 	"Springer-Verlag"
}

@TechReport{Joyce89,
   author = 	"Jeffrey J. Joyce",
   title = 	"A Verified Compiler for a Verified Microprocessor",
   institution = 	"University of Cambridge, Computer Laboratory",
   year = 	"1989",
   number = 	"167",
   month = 	mar
 }

@TechReport{Joyce90a,
  author = 	"Jeffrey J. Joyce",
  title = 	"Generic Specification of Digital Hardware",
  institution = "The University of British Columbia, Department of Computer
		 Science",
  year = 	"1990",
  number = 	"90--27",
  month = 	sep
}


% ----- K -----

@techreport{Matt,
     AUTHOR      = {Matthew J. Kaufmann},
     TITLE       = {A User's Manual for an Interactive Enhancement to 
                    the {B}oyer-{M}oore Theorem Prover},
     INSTITUTION = {CLInc},
     YEAR        = {1988},
     NUMBER      = {19},
     ANNOTE      = {}
     }

@techreport{Parallel,
     AUTHOR      = {Matthew J. Kaufmann and Matthew Wilding},
     TITLE       = {A Parallel Version of the {B}oyer-{M}oore Prover},
     INSTITUTION = {CLInc},
     YEAR        = {1989},
     NUMBER      = {39},
     ANNOTE      = {}
     }

@techreport{DEFN-SK,
     AUTHOR      = {Matt Kaufmann},
     TITLE       = {{DEFN-SK}: An {E}xtension of the {B}oyer-{M}oore {T}heorem
		    {P}rover to {H}andle {F}irst-{O}rder
                    {Q}uantifiers},
     INSTITUTION = {CLInc},
     YEAR        = {1989},
     NUMBER      = {43},
     ANNOTE      = {}
     } 

@Article{Generalization,
     author      = "Matt Kaufmann",
     title       = "Generalization in the Presence of Free Veriables: A
	            Mechanically-Checked Correctness Proof for one Algorithm",
     journal     = "Journal of Automated Reasoning",
     year        = "1991",
     volume      = "7",
     pages       = "109-159",
     note        = "",
     annote      = ""
     }

@Article{Kock90,
  author = 	"Gerd Kock",
  title = 	"Towards the Verification of Optimizing Transformations for
		 Imperative Programs",
  journal = 	"Microprocessing and Microprogramming",
  year = 	"1990",
  volume = 	"30",
  pages = 	"185-192"
}

@unpublished{LEXSynthesis,
     author      = {Kolyang and Junbo Liu and Burkhart Wolff},
     title       = {Transformational Development of {LEX}},
     institution = {University of Bremen, FB3 Informatik},
     note        = {Draft Manuscript for a {KORSO} - {K}orrekte {S}oftware
		  report}
     }
% ----- L -----
@PhdThesis{Lamb82,
  author = 	"Paul Arthur Lamb",
  title = 	"A verification condition generator for Intel 8080 microprocessor
		 assembly language programs",
  school = 	"George Washington University",
  year = 	"1982",
}

@book{LoeckxSieber,
     AUTHOR    = {Jacques Loeckx and Kurt Sieber},
     TITLE     = {The Foundations of Program Verification},
     PUBLISHER = {Wiley-Teubner},
     SERIES    = {Series in Computer Science},
     ADDRESS   = {Chichester, Stuttgart},
     YEAR      = {1987},
     ANNOTE    = {}
     }

% ----- M -----

@inproceedings{MacKenzie,
     AUTHOR      = {Donald Mac{K}enzie},
     TITLE       = {Formal Methods and the Sociology of Proof},
     BOOKTITLE   = {4th Refinement Workshop [{BCS-FACS}] 9-11 Jan 1991, Cambridge},
     EDITOR      = {J. M. Morris and Roger C. Shaw},
     PAGES       = {115-124},
     YEAR        = {1991},
     PUBLISHER   = {Springer Verlag},
     ADDRESS     = {Berlin}
     }

@InProceedings{Martin91,
  author = 	"D. Martin and R. Toal",
  title = 	"Case Studies in Compiler Correctness Using {HOL}",
  booktitle = 	"Proceedings of the 1991 International Workshop on the {HOL}
		 Theorem Proving System and its Applications",
  year = 	"1992",
  publisher = 	"{IEEE} Computer Society Press",
  note = 	"To be published."
}

 @InProceedings{Maurer76,
   author = 	"W. D. Maurer",
   title = 	"Proving the Correctness of a Flight-Director Program for an
		  Airborne Minicomputer",
   booktitle = 	"Proceedings of the {ACM SIGMINI/SIGPLAN} Interface Meeting on
		  Program Systems in the Small Processor Environment",
   year = 	"1976",
   pages = 	"103-108",
   note = 	"Appeared as a special issue of SIGPLAN Notice V11(4), April 1976"
 }

 @InProceedings{Maurer77,
   author = 	"W. D. Maurer",
   title = 	"An {IBM} 370 Assembly Language Verifier",
   booktitle = 	"Proceedings of the 16th Annual Technical Symposium on
		  Systems and Software: Operational Reliability and Performance
		  Assurance ",
   year = 	"1977",
   editor = 	"P. A. Willis",
   pages = 	"139-146",
   organization = 	"{ACM}",
   month = 	jun
 }

@inproceedings{McCarthy,
     AUTHOR      = {J. McCarthy and J. Painter},
     TITLE       = {Correctness of a compiler for arithmetic expressions},
     BOOKTITLE   = {Mathematical Aspects of Computer Science. Proc. Symp. Appl. Math},
     VOLUME      = {XIX},
     PAGES       = {33-41}, 
     PUBLISHER   = {American Mathematical Society},
     editor 	 = {J. T. Schwartz},
     YEAR        = {1967},
     NOTE        = {}
     }

@techreport{Otter,
     AUTHOR      = {William McCune},
     TITLE       = {{OTTER} 2.0 Users Guide},
     INSTITUTION = {Argonne NAtional Laboratory},
     MONTH       = {March},
     YEAR        = {1990},
     NUMBER      = {ANL-90/9},
     ANNOTE      = {}
     }
@InProceedings{McNerney91,
  author = 	"Timothy S. McNerney",
  title = 	"Verifying the Correctness of Compiler Transformations on
		 Basic Blocks using Abstract Interpretation",
  booktitle = 	"Proceedings of the Symposium on Partial Evaluation and
		 Semantics-based Program Manipulation",
  year = 	"1991",
  pages = 	"106-115",
  publisher = 	"{ACM} Press",
  month = 	jun
}

@InCollection{Melham87,
  author = 	"Thomas F. Melham",
  title = 	"Abstraction Mechanisms for Hardware Verification",
  booktitle = 	"{VLSI} Specification, Verification and Synthesis",
  publisher = 	"Kluwer Academic Publishers",
  year = 	"1988",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  chapter = 	"9",
  pages = 	"267--292"

}



@InCollection{Melham88a,
  author = 	"Thomas F. Melham",
  title = 	"Automating Recursive Type Definitions in Higher Order Logic",
  booktitle = 	"Current Trends in Hardware Verification and Automated
		 Theorem Proving",
  publisher = 	"Springer-Verlag",
  year = 	"1989",
  editor = 	"G. Birtwistle and P. A. Subrahmanyam",
  chapter = 	"9",
  pages = 	"341--386"
}


@Article{Milner72,
  author = 	"R. Milner and R. Weyhrauch",
  title = 	"Proving Compiler Correctness in a Mechanized Logic",
  journal = 	"Machine Intelligence",
  year = 	"1972",
  volume = 	"7",
  pages = 	"51-70"
}


@Misc{DEFSTAN0055,
  key = "MOD",
  title = 	"{M}O{D}: Interim Defence Standard 00-55 on the
                  Procurement of Safety
		  Critical Software in Defence Equipment",
  year = 	"1991"
}
                   
@techreport{PITON,
     AUTHOR      = {{J Strother} Moore},
     TITLE       = {Piton: A Verified Assembly-Level Language},
     INSTITUTION = {CLInc},
     YEAR        = {1988},
     NUMBER      = {22},
     ANNOTE      = {}
     }

@article{MooreMVLI,
     AUTHOR  = {{J Strother} Moore},
     TITLE   = {A Mechanically Verified Language Implementation},
     JOURNAL = {Journal of Automated Reasoning},
     YEAR    = {1989},
     VOLUME  = {5},
     NUMBER  = {4},
     MONTH   = {Dec},
     NOTE    = {also available as CLInc Technical Report 30, 1988}
     }

@article{CoCOMech,
     AUTHOR  = {Robin Milner and R. Weyhrauch},
     TITLE   = {Proving Compiler Correctness in a Mechanized Logic},
     JOURNAL = {Machine Intelligence},
     YEAR    = {1972},
     VOLUME  = {7},
     PAGES   = {51-70},
     ANNOTE  = {}
     }

% ----- N -----

@INPROCEEDINGS{NicoliPierre:94,
        AUTHOR             = {Nicoli, F\'elix and Pierre, Laurence},
        BOOKTITLE          = {{P}roceedings of {EURO-DAC'94} with
                             {EURO-VHDL'94}},
        MONTH              = sep,
        TITLE              = {{F}ormal {V}erification of {B}ehavioural {VHDL}
                              {S}pecifications : a {C}ase {S}tudy},
        YEAR               = {1994}
}


% ----- O -----

@misc{MKRP,
     AUTHOR       = {H.J. Ohlbach and J. Siekmann},
     TITLE        = {The {M}arkgraf-{K}arl-{R}efutation {P}rocedure},
     howpublished = {Artikel zur Festschrift von Alan Robinsons Geburtstag. Oxford Press},
     YEAR         = {1990},
     ANNOTE       = {}
     }

 @InProceedings{O'Neill88,
   author = 	"I. M. {O'Neill} and D. L. Clutterbuck and P. F. Farrow and P.
		  G. Summers and W. C. Dolman",
   title = 	"The Formal Verification of Safety-Critical Assembly Code",
   booktitle = 	"Proceedings of the IFAC Symposium on Safety of Computer
		  Control Systems 1988 (Safecomp '88) Safety Related Computers
		  in an Expanding Market",
   year = 	"1988",
   editor = 	"W. D. Ehrenberger",
   publisher = 	"Pergamon Press",
   month = 	"nov"
 }



% ----- P -----

@TechReport{Palsberg92a,
  author = 	"Jens Palsberg",
  title = 	"A Provably Correct Compiler Generator",
  institution = 	"Aarhus University Computer Science Department",
  year = 	"1992",
  number = 	"DAIMI PB-382"
}

@TechReport{Palsberg92b,
  author = 	"Jens Palsberg",
  title = 	"An Automatically Generated and  Provably Correct Compiler for
		 a Subset of {A}da",
  institution = 	"Aarhus University Computer Science Department",
  year = 	"1992",
  number = 	"DAIMI PB-383"
}


@techreport{Penner,
     AUTHOR      = {Volker Penner},
     TITLE       = {Entwicklung und {V}erifikation eines {S}canner {G}enerators mit dem
                    {G}ypsy {V}erification {E}nvironment},
     INSTITUTION = {RWTH Aachen},
     ADDRESS     = {Schriften zur Informatik und Angewandten Mathematik},
     YEAR        = {1983},
     NUMBER      = {86},
     ANNOTE      = {}
     }

@INPROCEEDINGS {Pierre:90,
        AUTHOR    = {Laurence Pierre},
        BOOKTITLE = {Formal VLSI Correctness Verification},
        EDITOR    = {Claesen, L.},
        PUBLISHER = {Elsevier},
        TITLE     = {The formal proof of sequential circuits described in
                     {CASCADE} using the {Boyer-Moore} Theorem Prover},
        YEAR      = {1990}
        }


@INPROCEEDINGS{Pierre:93,
author = {Laurence Pierre},
title = {{VHDL} description and formal verification of systolic multipliers},
booktitle = {IFIP Conference on Hardware Description Languages
          and their applications},
address = {Ottawa, {C}anada},
month = {April},
year = 1993}


@INPROCEEDINGS{Pierre:94,
        AUTHOR             = {Pierre, Laurence},
        ADDRESS            = {Bad {H}errenalb ({B}lackforest), {G}ermany},
        BOOKTITLE          = {{T}heorem {P}rovers in {C}ircuit {D}esign},
        MONTH              = {September},
        TITLE              = {An automatic generalization method for the 
                  inductive proof of replicated and parallel architectures},
        YEAR               = {1994}
}

@TechReport{Plotkin81,
  author = 	"Gordon D. Plotkin",
  title = 	"A structural Approach to Operational Semantics",
  institution = 	"University of Aarhus, Denmark, Computer Science
		 Department ",
  year = 	"1981",
  OPTmonth = 	"September"
}


% ----- R -----
@phdthesis{Reif,
     AUTHOR      = {Wolfgang Reif},
     TITLE       = {Korrektheit von {S}pezifikationen und generischen {M}oduln},
     SCHOOL      = {Universit\"at Karlsruhe},
     YEAR        = {1991},
     ANNOTE      = {Zahlen \"uber Anzahl von Beweisschritte}
     }

@mastersthesis{WilsonTheorem,
     AUTHOR      = {David M. Russinoff},
     TITLE       = {A Mecanical Proof of Wilson's Theorem},
     INSTITUTION = {University of Texas at Austin, Department of
                    Computer Science},
     YEAR        = {1983}
     }

@article{QuadraticReciprocity,
     AUTHOR      = {David M. Russinoff},
     TITLE       = {A Mechanical Proof of Quadratic Reciprocity},
     JOURNAL     = {Journal of Automated Reasoning},
     VOLUME      = {8},
     NUMBER      = {1},
     YEAR        = {1992},
     PAGES       = {???}
     }
      



% ----- S -----

@techreport{ZEVES,
     AUTHOR      = {Mark Saaltink},
     TITLE       = {{Z} and {EVES}},
     INSTITUTION = {Odyssey Research Association},
     ADDRESS     = {Ottawa,Ontario},
     MONTH       = {October}, 
     YEAR        = {1991},
     NUMBER      = {TR-91-5449-02},
     ANNOTE      = {}
     }

@techreport{Shankar,
     AUTHOR      = {N. Shankar},
     TITLE       = {A Mechanical Proof of the {C}hurch-{R}osser Theorem},
     INSTITUTION = {University of Texas, Institute for Computer Science},
     ADDRESS     = {Austin, Texas},
     MONTH       = {March},
     YEAR        = {1985},
     NUMBER      = {45},
     ANNOTE      = {}
     }

@phdthesis{Shankar1,
     AUTHOR      = {N. Shankar},
     TITLE       = {Proof Checking Metamathematics},
     SCHOOL      = {Univ. of Texas, Austin},
     YEAR        = {1986},
     ANNOTE      = {Goedel's incompleteness theorem, u.a.}
     }

@TechReport{Silva92,
  author = 	"Fabio Q. B. da Silva",
  title = 	"Correctness Proofs of Compilers and Debuggers: an Overview of
		 an Approach Based on Structural Operational Semantics ",
  institution = 	"Department of Computer  Science, University of
		 Edinburgh",
  year = 	"1992",
  number = 	"ECS-LFCS-92-233",
  month = 	"September"
}

@TechReport{Simpson91,
  author = 	"Todd G. Simpson",
  title = 	"Design and Verification of {IFL}: a Wide-Spectrum
		 Intermediate Functional Language",
  institution = 	"Univesity of Calgary, Department of Computer Science",
  year = 	"1991",
  number = 	"91/440/24",
  month = 	jul
}

@Article{Stepney91,
  author = 	"Susan Stepney and Dave Whitley and David Cooper and Colin Grant",
  title = 	"A Demonstrably Correct Compiler",
  journal = 	"Formal Aspects of Computing",
  year = 	"1991",
  volume = 	"3",
  pages = 	"58--101",
  note = 	""
}




% ----- T -----

@article{BagsToSets,
     AUTHOR      = {Jukka Teuhola and Lutz Wegner},
     TITLE       = {Minimal space average linear time duplication deletion},
     JOURNAL     = {CACM},
     VOLUME      = {34},
     NUMBER      = {3},
     MONTH       = {March},
     YEAR        = {1991},
     PAGES       = {62-73},
     ANNOTE      = {specification for WrongVerification}
     }

@Article{Thatcher81,
  author = 	"James W. Thatcher and Eric G. Wagner and Jesse B. Wright",
  title = 	"More on Advice on Structuring Compilers and Proving them Correct",
  journal = 	"Theoretical Computer Science",
  year = 	"1981",
  volume = 	"15",
  pages = 	"223-249",
  note = 	""
}

% ----- V -----

@INPROCEEDINGS {ifip:90,
        AUTHOR    = {Verkest, D. and Claesen, L. and De Man, H.},
        BOOKTITLE = {Formal VLSI Specification and Synthesis: VLSI
                     Design Methods I},
        EDITOR    = {Claesen, L. J. M.},
        PAGES     = {99 - 116},
        PUBLISHER = {Elsevier},
        TITLE     = {On the Use of the {Boyer-Moore} Theorem Prover for
                     Correctness Proofs of Parameterized Hardware Modules},
        YEAR      = {1990}
        }

@INPROCEEDINGS {edac:90,
        AUTHOR    = {Verkest, D. and Claesen, L. and De Man, H.},
        BOOKTITLE = {Proceedings of EDAC-90},
        MONTH     = {March},
        PAGES     = {62 - 66},
        TITLE     = {Correctness Proofs of Parameterized Hardware Modules
                     in the {Cathedral-II} Synthesis Environment},
        YEAR      = {1990}
        }

@INPROCEEDINGS {dcc:92,
        AUTHOR    = {Verkest, D. and Claesen, L. and De Man, H.},
        BOOKTITLE = {IFIP Transactions A-5: Designing Correct Circuits},
        EDITOR    = {Staunstrup, J. and Sharp, R.},
        PAGES     = {173 - 192},
        PUBLISHER = {Elsevier},
        TITLE     = {A Proof of the {Non Restoring Division} Algorithm and
                     its Implementation on the {Cathedral-II ALU}},
        YEAR      = {1992},
        ANNOTE    = {}
        }

@INPROCEEDINGS {tpcd:92,
        AUTHOR    = {Verkest, D. and Vandenbergh, J. and Claesen, L.
                     and De Man, H.},
        BOOKTITLE = {IFIP Transactions A-10: Theorem Provers in Circuit Design},
        EDITOR    = {Stavridou, V. and Melham, T. F. and Boute, R. T.},
        PAGES     = {37 - 57},
        PUBLISHER = {Elsevier},
        TITLE     = {A Description Methodology for Parameterized
                     Modules in the {Boyer-Moore} Logic},
        YEAR      = {1992},
        ANNOTE    = {This is an attempt at explaining how he models the hardware modules
                     in the theorem prover. Basically it discusses the cosmetical changes to
                     Warren Hunt's description style.}
        }


% ----- W -----


@techreport{DWW5,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Proof Movie : Proving the Add-Assign Compiler with
                    the {B}oyer-{M}oore Prover},
     INSTITUTION = {ProCoS},
     ADDRESS     = {Kiel},
     MONTH       = {July},
     YEAR        = {1990},
     NUMBER      = {DWW 5},
     NOTE        = {A revised version of this report has been accepted by ``Formal Aspects of Computing''
                    for publication}
     }


@article{dwwFAC,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Proof Movie : A {P}roof with the {B}oyer-{M}oore Prover},
     PUBLISHER   = {British Computer Society},
     JOURNAL     = {Formal Aspects of Computing},
     VOLUME      = {5},
     YEAR        = {1993},
     PAGES       = {121-151}
     }

@techreport{DWW10,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {When Whitespace Conveys Meaning},
     INSTITUTION = {TFH Berlin},
     ADDRESS     = {Berlin},
     MONTH       = {October},
     YEAR        = {1992},
     NUMBER      = {DWW 10},
     ANNOTE        = {rejected by POPL'93, ``ACM SIGPLAN'93''}
     }

@techreport{Scanning,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Proven-Correct Scanning},
     INSTITUTION = {ProCoS},
     ADDRESS     = {Kiel},
     MONTH       = {October},
     NUMBER      = {DWW 11/1},
     YEAR        = {1992},
     NOTE        = {Report on the suspended proof effort for scanning}
     }




% ----- Y -----

@techreport{YoungSmall,
     AUTHOR      = {William D. Young},
     TITLE       = {A Verified Code Generator for a Subset of {G}ypsy},
     INSTITUTION = {CLInc},
     YEAR        = {1988},
     NUMBER      = {33},
     ANNOTE      = {}
     }

@article{YoungMicroGypsy,
     AUTHOR  = {William D. Young},
     TITLE   = {A Mechanically Verified Code Generator},
     JOURNAL = {Journal of Automated Reasoning},
     YEAR    = {1989},
     VOLUME  = {5},
     NUMBER  = {4},
     MONTH   = {Dec},
     NOTE    = {also available as CLInc Technical Report 37 , 1989}
     }

@misc{YoungFSAProof,
     AUTHOR    = {William D. Young},
     TITLE     = {A Mechanically Checked Proof of the Equivalence of
                  Deterministic and Non-Deterministic Finite State
		  Machines},
     YEAR      = {1993},
     MONTH     = {October 19,},
     NOTE      = {CLInc Internal Note \#290},
     ANNOTE    = {Bill's existential proof}
     }


@techreport{YuanYu,
    AUTHOR      = { R. S. Boyer and Y. Yu},
    TITLE       = {Automated Correctness Proofs of Machine Code Programs
                   for a Commercial Microprocessor},
    INSTITUTION = {Computer Science Dept., University of Texas,
		  Austin},
    NUMBER      = {TR-91-33},
    MONTH       = {November},
    YEAR        = {1991}
    }
    

@article{YuGroup,
    Author      = {Yuan Yu},
    Title       = {Computer Proofs in Group Theory},
    Journal     = {Journal of Automated Reasoning},
    Year        = {1990},
    Volume      = {6},
    Pages       = {251-286}
    }