%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%		  
% Fuer VERIFIX relevante Fremdpublikationen
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Schluesselaenderungen:
% Palsberg92 -> Palsberg92a
%	     -> Palsberg92b
%
% BlumKannan:1995 -> Blum:1995:DPC (doppelt)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%		  
% Stringdefinition, die schon aufgeloest sind.
%
% @STRING{toplas = {ACM Transactions on Programming Languages and Systems} } 
% @STRING{sigplannot={{ACM SIGPLAN} Notices} }
% @STRING{jpldi	= {Journal of Programming Languages} }
% @STRING{pldi	= {{ACM SIGPLAN} Conference on Programming Language Design
% 		  and Implementation} }
% @STRING{esop	= {European Symposium on Programming (ESOP)} }
% @STRING{tapsoft = {International Joint Conference on the Theory and Practice 
%		  of Software Development (TAPSOFT)} }
% @STRING{cc	= {Conference on Compiler Construction (CC)} }
% @STRING{mfcs	= {Conference on the Mathematical Foundations of Computer
% 		  Science (MFCS)} }
% @STRING{cacm	= "Communications of the ACM" }
% @STRING{lncs	= "Lecture Notes in Computer Science" }
%
%
		  
@TechReport{	 Abecker+95,
  author =	 {Andreas Abecker and Harold Boley and Knut Hinkelmann
                  and Holger Wache and Franz Schmalhofer},
  institution =	 {DFKI GmbH},
  month =	 nov,
  title =	 {{An Environment for Exploring and Validating
                  Declarative Knowledge}},
  type =	 {{DFKI Technical Memo TM-95-03}},
  note =	 {Also in: Proc. Workshop on Logic Programming
                  Environments at ILPS'95, Portland, Oregon,
                  Dec. 1995},
  year =	 1995
}

@Booklet{	 Abelson+86,
  author =	 {{Abelson, H. et. al.}},
  title =	 {$\mbox{Revised}^3\,\mbox{Report}$ on the
                  {A}lgorithmic {L}anguage {SCHEME}},
  howpublished = {J.~Rees, W.~ Clinger (Hrsg.)},
  year =	 1986
}

@TechReport{	 Ackermann+88,
  author =	 {Ackermann, D. and Goerigk, W. and Simon, F.},
  title =	 {Kompilation von {Wissensrepr\"asentationssprachen}
                  am {Beispiel} von {BABYLON}},
  institution =	 {Institut f\"ur Informatik, CAU},
  note =	 {Ebenfalls erschienen als Kapitel 8 in
                  \cite{Christaller+89}},
  type =	 {Institutsbericht},
  number =	 {Nr. 8810},
  address =	 {Kiel},
  year =	 1988
}

@InProceedings{	 Ackermann+89,
  author =	 {Ackermann, D. and Goerigk, W. and Simon, F.},
  editor =	 {Christaller, Th. and diPrimio, F. and Vo{\ss}, A.},
  title =	 {{W}issensbasiskompilation},
  booktitle =	 {Die {KI--W}erkbank {BABYLON}},
  publisher =	 {Addison--Wesley},
  address =	 {Bonn},
  year =	 1989
}

@Article{	 Ackermann+91,
  author =	 {Ackermann, D. and Goerigk, W. and Simon, F.},
  title =	 {{W}issensbasiskompilation: {KI}-{T}echnik in
                  industrieller {A}nwendung},
  journal =	 {KI},
  year =	 1991,
  volume =	 91,
  number =	 2,
  pages =	 {93-96},
  address =	 {{B}aden {B}aden},
  month =	 jun
}

@InProceedings{	  Ackermann/Goerigk87a,
  author	= {Ackermann, D. and Goerigk, W.},
  title		= {Das {Projekt}: {\"Ubersetzung} von {Wissensbasen}},
  booktitle	= {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und
		  Rechner''}},
  address	= {Bad Honnef},
  year		= 1987
}

@InProceedings{	  Ackermann/Goerigk87b,
  author =	 {Ackermann, D. and Goerigk, W.},
  title =	 {{\"Ubersetzung} von {PROLOG} nach {LISP}},
  booktitle =	 {Work\-shop {\sl ``Alternative Konzepte f\"ur
                  Sprachen und Rechner''}},
  address =	 {Bad Honnef},
  year =	 1987
}

@PhDThesis{	  Ackermann91,
  author =	 {Ackermann, D.},
  title =	 {{A}nalyse {p}olymorpher {T}ypen {b}ei {l}ogischen
                  {P}rogrammiersprachen {m}ittels
                  {S}ubstitutionsgrammatiken},
  school =	 {Math.--Nat. Fakult\"at der
                  Christian-Albrechts-Universit\"at},
  address =	 {{K}iel},
  note =	 {Institutsbericht Nr. 9101 des Instituts f\"ur
                  Informatik und Prakt. Mathematik der CAU Kiel},
  year =	 1991
}

@TechReport{	  Assmann93d,
  author	= {A{\ss}mann, Uwe},
  title		= {Edge Addition Rewrite Systems And Their Relevance to
		  Program Analysis},
  institution	= {GMD Forschungsstelle Karlsruhe},
  type		= {{I}nterner {B}ericht},
  year		= {1993}
}

@PhDThesis{	  Assmann94a,
  author	= {A{\ss}mann, Uwe},
  title		= {Konfluente Graphersetzungssysteme und ihre Anwendung auf
		  Programmoptimierung},
  school	= {Universit\"at Karlsruhe},
  year		= {1994},
  address	= {Kaiserstr. 12, 7500 Karlsruhe, Germany},
  month		= {}
}

@Article{	  Attardi95,
  author	= {Giuseppe Attardi},
  title		= {{The Embeddable Common Lisp}},
  journal	= {LISP Pointers},
  volume	= {VIII},
  number	= {1},
  pages		= {30-41},
  publisher	= {ACM Press},
  year		= {1995}
}

@Article{	  BD96,
  author	= {E. B{\"o}rger and I. Durdanovic},
  title		= {Correctness of Compiling Occam to Transputer},
  journal	= {The Computer Journal},
  year		= {1996},
  volume	= {39},
  number	= {1},
  pages		= {52--92}
}

@Misc{		  BPvHR99,
  author	= {M. Bartels and H. Pfeifer and F.W. von Henke and H.
		  Rue{\ss}},
  title		= {Mechanizing Domain Theory},
  year		= {1999},
  note		= {submitted to the journal ``Applied Categorical
		  Structures}
}

@Misc{		  BSI94,
  author	= {{BSI-Bundesamt f\"ur Sicherheit in der
		  Informationstechnik}},
  title		= {{BSI-Zertifizierung}},
  howpublished	= {BSI 7119, Bonn},
  year		= {1994}
}

@InProceedings{	  Baker90,
  author	= {Baker, H.},
  title		= {{T}he {NIMBLE} {P}roject -- {A}n {A}pplications {C}ompiler
		  for {R}eal-{T}ime {C}ommon {L}isp},
  booktitle	= {Proceedings of the InfoJapan '90 Conf.},
  publisher	= {Info. Proc. Soc. Japan},
  address	= {Tokyo},
  year		= {1990}
}

@Book{		  Best,
  author	= {E. Best},
  title		= {Semantik -- Theorie sequentieller und paralleler
		  Programmierung},
  publisher	= {Vieweg-Verlag},
  year		= {1995},
  series	= {Lehrbuch Informatik}
}

@Book{		  Bibel87,
  author	= {Wolfgang Bibel},
  edition	= {Second},
  publisher	= {Vieweg},
  title		= {Automated Theorem Proving},
  year		= {1987}
}

@Book{		  Birtwistle+73,
  author	= {Birtwistle, G. and Dahl, {O.J.} and Myhrhaug, B. and
		  Nygaard, K.},
  title		= {{SIMULA} {BEGIN}},
  publisher	= {Auerbach},
  address	= {Philadelphia},
  year		= {1973}
}

@Book{		  Bittel91,
  author	= {O. Bittel},
  title		= {Ein tableaubasierter Theorembeweiser f{\"u}r
		  intuitonistische Logik},
  series	= {GMD--Berichte},
  publisher	= {Oldenbourg-Verlag},
  volume	= {198},
  year		= {1991}
}

@Book{		  Bjoerner+93,
  editor	= {Dines {Bj\o rner} and Hans Langmaack and {C.A.R.} Hoare},
  title		= {{P}rovably {C}orrect {S}ystems -- {ProCoS}, {ESPRIT BRA
		  3104}},
  publisher	= {Dep.\ of\ Computer Science, Techn. Univ. of Denmark},
  year		= {1993},
  note		= {Monograph, Final Deliverable}
}

@Book{		  Bjoerner91,
  key		= {Bjo},
  author	= {Dines Bj{\o rner}},
  title		= {{F}inal {R}eport {ProCoS} - {P}rovably {C}orrect
		  {S}ystems, {ESPRIT BRA 3104}},
  publisher	= {Dep.\ of\ Computer Science, Techn. Univ. of Denmark},
  year		= {1991}
}

@InProceedings{	  Blum+89,
  author	= {M. Blum and M. Luby and R. Rubinfeld},
  title		= {Program Result Checking Against Adaptive Programs and in
		  Cryptographic Settings},
  booktitle	= {DIMACS Workshop on Distributed Computing and
		  Crypthography},
  year		= {1989}
}

@InProceedings{	  Blum+90,
  author	= {M. Blum and M. Luby and R. Rubinfeld},
  title		= {Self--Testing/Correcting with Applications to Numerical
		  Problems},
  booktitle	= {Proceedings 22nd Symposium on Theory of Computing},
  year		= {1990}
}

@InProceedings{   Blum/Kannan89,
  author	= {M. Blum and S. Kannan},
  title		= {Program Correctness Checking $\ldots$ and the Design of
		  Programs that check their Work},
  booktitle	= {Proceedings 21st Symposium on Theory of Computing},
  year		= {1989}
}

@Article{	  BlumKannan:1995,
  crossref	= {Blum:1995:DPC}
}

@Article{	  Blum:1995:DPC,
  author	= {Manuel Blum and Sampath Kannan},
  title		= {Designing Programs that Check Their Work},
  journal	= {Journal of the Association for Computing Machinery},
  volume	= {42},
  number	= {1},
  pages		= {269--291},
  month		= jan,
  year		= {1995},
  abstract	= {A {\em program correctness checker\/} is an algorithm for
		  checking the output of a computation. That is, given a
		  program and an instance on which the program is run, the
		  checker certifies whether the output of the program on that
		  instance is correct. This paper defines the concept of a
		  program checker. It designs program checkers for a few
		  specific and carefully chosen problems in the class FP of
		  functions computable in polynomial time. Problems in FP for
		  which checkers are presented in this paper include Sorting,
		  Matrix Rank and GCD. It also applies methods of modern
		  cryptography, especially the idea of a probabilistic
		  interactive proof, to the design of program checkers for
		  group theoretic computations.\par Two structural theorems
		  are proven here. One is a characterization of problems that
		  can be checked. The other theorem establishes equivalence
		  classes of problems such that whenever one problem in a
		  class is checkable, all problems in the class are checkable.}
}

@InCollection{	  BoeSch98a,
  author	= {E. B\"orger and W. Schulte},
  title		= {{Programmer Friendly Modular Definition of the Semantics
		  of Java}},
  booktitle	= {{Formal Syntax and Semantics of Java}},
  publisher	= {Springer},
  year		= {1998},
  editor	= {J. Alves-Foss},
  series	= {LNCS}
}

@InCollection{	  BoeSch98b,
  author	= {E. B\"orger and W. Schulte},
  title		= {{A Modular Design for the Java VM architecture}},
  booktitle	= {{Architecture Design and Validation Methods}},
  publisher	= {Springer},
  year		= {1998},
  editor	= {E. B\"orger}
}

@InCollection{	  BoeSch98c,
  author	= {E. B\"orger and W. Schulte},
  title		= {{Defining the Java Virtual Machine as Platform for
		  Provably Correct Java Compilation}},
  booktitle	= {{23rd International Symposium on Mathematical Foundations
		  of Computer Science}},
  publisher	= {Springer},
  series	= {LNCS},
  year		= {1998},
  note		= {To appear}
}

@InCollection{BoeMaz97, 
  author =       "E. B{\"o}rger and S. Mazzanti", 
  title =        "{A Practical Method for Rigorously Controllable 
                  Hardware Design}", 
  booktitle =    "{ZUM'97: The Z Formal Specification Notation}",
  publisher =    "Springer", 
  year =         "1997", 
  editor =       "J.P. Bowen and M.B. Hinchey and D. Till",
  volume =       "1212", 
  series =       "LNCS", 
  pages =        "151-187"
}

@Book{		  Boerger/Rosenzweig92,
  author	= {B\"orger, E. and Rosenzweig, D.},
  title		= {{T}he {WAM}-definition and {C}ompiler {C}orrectness},
  publisher	= {Beierle, L.C. and Pluemer, L.},
  year		= {1994},
  booktitle	= {Logic Programming: Formal Methods and Practical
		  Applications},
  series	= {North-Holland Series in Computer Science and Artificial
		  Intelligence}
}

@InProceedings{BoDeGR94, 
  author =       "E. B{\"o}rger and G. {Del Castillo} and P. Glavan 
                  and D. Rosenzweig", 
  title =        "{Towards a Mathematical Specification of the APE100 
                  Architecture: the APESE Model.}", 
  editor =       "B. Pehrson and I. Simon", 
  volume =       "I: Technology/Foundations", 
  pages =        "396-401", 
  booktitle =    "IFIP 13th World Computer Congress", 
  year =         "1994", 
  address =      "Elsevier, Amsterdam, the Netherlands"
} 

@Article{	  Boerger96,
  author	= {E. B{\"o}rger and I. Durdanovic},
  title		= {{C}orrectness of {C}ompiling {O}ccam to {T}ransputer
		  code},
  journal	= {The Computer Journal},
  year		= {1996},
  volume	= {39},
  pages		= {52-93}
}

@InProceedings{	  BoergerEgo1994a,
  author	= {E. B{\"o}rger and I. Durdanovic and D. Rosenzweig},
  booktitle	= {Proc. Procomet'94 (IFIP TC2 Working Conference on
		  Programming Concepts, Methods and Calculi)},
  title		= {{O}ccam: {S}pecification and {C}ompiler
		  {C}orrectness.{P}art {I}: {T}he {P}rimary {M}odel},
  year		= {1994},
  abstract-url	= {ftp://ftp.di.unipi.it/pub/Papers/boerger/01ABSTRACTS},
  url		= {ftp://ftp.di.unipi.it/pub/Papers/boerger/310occam1.ps.Z},
  editor	= {U. Montanari and E.-R. Olderog},
  publisher	= {North-Holland},
  scope		= {occam}
}

@InProceedings{	  Boley92b,
  author	= {Harold Boley},
  booktitle	= {Proceedings of the 2nd International Workshop on
		  Extensions of Logic Programming, ELP '91, Stockholm 1991},
  publisher	= {Springer-Verlag},
  series	= {LNAI},
  title		= {{Extended Logic-plus-Functional Programming}},
  volume	= {596},
  year		= {1992},
  editor	= {Eriksson, Lars-Henrik and Halln{\"a}s, Lars and
		  Schroeder-Heister, Peter}
}

@InProceedings{	  Bowen+90,
  author	= {J. Bowen and H. Jifeng and P. Pandya},
  title		= {An Approach to verifiable compiling Specification and
		  Prototyping},
  booktitle	= {Proceedings of PLILP 90},
  series	= {LNCS},
  volume	= {456},
  year		= {1990},
  publisher	= {Springer-Verlag}
}

@Article{	  Bowen+96,
  author	= {J. Bowen and {C. A. R.} Hoare and H. Langmaack and {E.-R.}
		  Olderog and {A. P.} Ravn},
  title		= {{A ProCoS II Project Final Report: ESPRIT Basic Reserach
		  Project 7071}},
  journal	= {EATCS-Bulletin},
  year		= {1996}
}

@InProceedings{	  Bowen92,
  author	= {Jonathan P.~Bowen},
  title		= {{F}rom {P}rograms to {O}bject {C}ode {U}sing {L}ogic and
		  {L}ogic {P}rogramming},
  editor	= {R.~Giegerich and S.~Graham},
  booktitle	= {Proceedings CODE '91 International Workshop on Code
		  Generation},
  series	= {Workshops in Computing},
  year		= {1992},
  publisher	= {Springer-Verlag},
  address	= {Schlo\ss\ Dagstuhl}
}

@TechReport{	  Boyer/Moore77,
  author	= {{R.S.} Boyer and {J S.} Moore},
  institution	= {SRI International},
  number	= {5},
  title		= {A computer proof of the correctness of a simple optimizing
		  compiler for expressions},
  year		= {1977}
}

@Book{		  Boyer/Moore79,
  author	= {{R.S.} Boyer and {J S.} Moore},
  publisher	= {Academic Press Inc.},
  title		= {A Computational Logic},
  year		= {1979}
}

@Book{		  Boyer/Moore81,
  author	= {{R.S.} Boyer and {J S.} Moore},
  publisher	= {Academic Press Inc.},
  title		= {The Correctness Problem in Computer Science},
  address 	= {London, England},
  year		= {1981}
}

@Article{	  Brauer93,
  author	= {Brauer, Wilfried},
  title		= {{KI} auf dem {W}eg in die {N}ormalit\"at},
  journal	= {KI},
  year		= {1993},
  volume	= {Sonderheft},
  pages		= {85-91},
  month		= aug
}

@Article{	  Bretthauer+92,
  author	= {Bretthauer, Harry and Christaller, Thomas and Friedrich,
		  Horst and Goerigk, Wolfgang and Heicking, Winfried and
		  Hoffmann, Ulrich and Hovekamp, Dieter and Knutzen, Heinz
		  and Kopp, J\"urgen and Kriegel, {E. Ulrich} and Mohr, Ingo
		  and Rosenm\"uller, Rainer and Simon, Friedemann},
  title		= {{D}as {V}erbundvorhaben {APPLY}: {E}in modernes und
		  bedarfsgerechtes {L}isp},
  journal	= {KI},
  year		= {1992},
  volume	= {2},
  pages		= {50-54},
  month		= jun
}

@TechReport{	  Bretthauer+94,
  author	= {Bretthauer, Harry and Christaller, Thomas and Friedrich,
		  Horst and Goerigk, Wolfgang and Heicking, Winfried and
		  Hoffmann, Ulrich and Kind, Andreas and Klude, Bert and
		  Knutzen, Heinz and Kopp, J\"urgen and Kriegel, E. Ulrich
		  and Mohr, Ingo and Rosenm\"uller, Rainer and Simon,
		  Friedemann},
  title		= {{V}on der {APPLY}-{M}ethodik zum {S}ystem},
  institution	= {CAU/GMD/ISST/VW-GEDAS},
  type		= {Abschlu\ss bericht des BMFT-Projektes APPLY},
  number	= {APPLY/XIII/10},
  address	= {Sankt Augustin},
  year		= {1994},
  month		= jun
}

@InProceedings{	  Brown+92,
  author	= {D. F. Brown and H. Moura and D. A. Watt},
  title		= {Actress: an Action Semantics Directed Compiler Generator},
  series	= {LNCS},
  volume	= {641},
  booktitle	= {Compiler Compilers 92},
  year		= {1992}
}

@InProceedings{	  Brown-et-al:92,
  author	= {D. F. Brown and H. Moura and D. A. Watt},
  title		= {Actress: an Action Semantics Directed Compiler Generator},
  series	= {Lecture Notes in Computer Science},
  volume	= {641},
  booktitle	= {Compiler Compilers 92},
  year		= {1992}
}
@TechReport{	  Broy92,
  author	= {M. Broy},
  institution	= {Digital Systems Research Center},
  title		= {Experiences with Software Specification and Verification
		  using LP, the Larch Proof Assistant},
  year		= {1992}
}

@Book{		  Burghardt93,
  author	= {J. Burghardt},
  title		= {Eine feink{\"o}rnige Sortendisziplin und ihre Anwendung in
		  der Programmkonstruktion},
  series	= {GMD--Berichte},
  volume	= {212},
  publisher	= {Oldenbourg-Verlag},
  year		= {1993}
}

@InProceedings{	  Burkart+91,
  author	= {Burkart, O. and Goerigk, W. and Knutzen, H.},
  title		= {{CLiCC}: {A} {N}ew {A}pproach to the {C}ompilation from
		  {C}ommon {L}isp {P}rograms to {C}},
  booktitle	= {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und
		  Rechner''}},
  address	= {Bericht Nr.\ 8/91-I des Instituts f\"ur angewandte
		  Mathematik und Informatik der Univ.\ M\"unster},
  year		= {1991}
}

@MastersThesis{	  Burkart91,
  author	= {Burkart, Olaf},
  title		= {{D}as {F}rontend {e}ines {C}ompilers {v}on {Common Lisp}
		  {n}ach {C}},
  school	= {Institut f\"ur Informatik, CAU},
  address	= {{K}iel},
  year		= {1991}
}

@Article{	  Burn+86,
  author	= {Burn, G. and Hankin, C. and Abramsky, S},
  title		= {Strictness analysis for higher order functions},
  journal	= {Sci. Comput. Programm.},
  volume	= {7},
  pages		= {249--278},
  year		= {1986}
}

@InCollection{	  Burstall/Landin69,
  author	= {R. M. Burstall and P.J. Landin},
  title		= {Programs and their proofs: an algebraic approach},
  booktitle	= {Machine Intelligence 4},
  editor	= {B. Meltzer and D. Michie},
  publisher	= {Edinburgh University Press},
  year		= {1969}
}

@InProceedings{	  Buth+92,
  author	= {B. Buth and K.-H. Buth and M. Fr\"anzle and {B. v.} Karger
		  and Y. Lakhneche and H. Langmaack and M. M\"uller-Olm},
  title		= {Provably correct compiler development and implementation},
  editor	= {U. Kastens and P. Pfahler},
  booktitle	= {Compiler Construction},
  series	= {LNCS},
  volume	= {641},
  publisher	= {Springer-Verlag},
  year		= {1992}
}

@InProceedings{	  Buth/Mueller-Olm93,
  author	= {B. Buth and M. M\"uller-Olm},
  title		= {{P}rovably {C}orrect {C}ompiler {I}mplementation},
  pages		= {451--465},
  booktitle	= {{T}utorial {M}aterial -- {F}ormal {M}ethods {E}urope '93},
  year		= {1993},
  organization	= {IFAD Odense Teknikum},
  address	= {Denmark},
  month		= apr
}

@InCollection{	  Buth92b,
  author	= {{K.-H.} Buth},
  title		= {Using SOS Definitions in Term Rewriting Proofs},
  booktitle	= {First International Workshop on Larch, Dedham 1992},
  publisher	= {Springer-Verlag},
  editor	= {Ursula Martin and Jeanette M. Wing},
  year		= {1993},
  series	= {Workshops in Computing},
  pages		= {36--54}
}

@Unpublished{	  CMR:1996,
  author	= {D. Cyrluk,O. M{\"o}ller,H.Rue{\ss}},
  title		= {An {E}fficient {D}ecision {P}rocedure for the {T}heory of
		  {B}itvectors with {C}omposition and {E}xtraction},
  address	= {Abtl. K{\"u}nstliche Intelligenz, Universit{\"a}t Ulm,
		  89069-Ulm, Germany}
}

@InProceedings{	  CRSS94,
  author	= {D. Cyrluk and S. Rajan and N. Shankar and M. K. Srivas},
  title		= {{Effective theorem proving for hardware verification}},
  year		= {1994},
  booktitle	= {{Theorem Provers in Curcuit Design (TPCD '94)}},
  editor	= {R. Kumar, T. Kropf},
  volume	= {910},
  series	= {LNCS},
  publisher	= {Spcringer-Verlag},
  month		= {September}
}

@InProceedings{	 Cardelli84,
  author =	 {Cardelli, L.},
  editor =	 {Kahn, G. and MacQueen, {D.B.} and Plotkin, G.},
  title =	 {A {S}emantics of {M}ultiple {I}nheritance},
  booktitle =	 {Intern. Symposium on Semantics of Data Types,
                  Lecture Notes in Computer Science No. 173},
  publisher =	 {Springer-Verlag},
  pages =	 {51--68},
  address =	 {Berlin, Heidelberg, New York},
  year =	 {1984}
}

@Article{	 Chirica/Martin86,
  author =	 {Chirica, {L.M.} and Martin, {D.F.}},
  title =	 {{Toward Compiler Implementation Correctness Proofs}},
  journal =	 {ACM Transactions on Programming Languages and
                  Systems},
  volume =	 {8},
  number =	 {2},
  month =	 apr,
  pages =	 {185--214},
  year =	 {1986}
}

@Book{		  Christaller+89,
  editor	= {Christaller, Th. and diPrimio, F. and Vo{\ss}, A.},
  title		= {Die {KI--W}erkbank {BABYLON}},
  publisher	= {Addison--Wesley},
  address	= {Bonn},
  year		= {1989}
}

@inproceedings{	 Cimatti+97,
  author =	 {Alessandro Cimatti and Fausto Giunchiglia and Paolo
                  Pecchiari and Bruno Pietra and Joe Profeta and Dario
                  Romano and Paolo Traverso and Bing Yu},
  title =	 {A Provably Correct Embedded Verifier for the
                  Certification of Safety Critical Software},
  booktitle =	 {CAV'97},
  address =	 {Haifa, Israel},
  editor =	 {Orna Grumberg},
  pages =	 {202--213},
  publisher =	 {Springer-Verlag},
  series =	 {Lecture Notes in Computer Science},
  volume =	 {1254},
  year =	 {1997},
}

@InProceedings{	  Cohn79a,
  author	= {A. Cohn},
  booktitle	= {Proceedings of the Fifth Symposium on Automated
		  Deduction},
  title		= {High Level Proof in LCF},
  year		= {1979}
}

@PhDThesis{	  Cohn79b,
  author	= {A. Cohn},
  school	= {University of Edinburgh},
  title		= {Machine Assisted Proofs of Recursion Implementation},
  year		= {1979}
}

@Book{		  Constable+86,
  author	= {R. L. {Constable et al.}},
  publisher	= {Prentice-Hall},
  title		= {Implementing Mathematics with the Nuprl Proof Development
		  System},
  year		= {1986}
}

@Article{	  Cooper72a,
  author	= {D.C. Cooper},
  journal	= {Machine Intelligence},
  pages		= {91-99},
  title		= {Theorem Proving in arithmetic without multiplication},
  volume	= {7},
  year		= {1972},
  category	= {DecisionProcedures}
}

@Article{	  Coquand+94,
  author	= {T. Coquand and B. Nordstr\"om and J.M. Smith and B. von
		  Sydow},
  journal	= {EATCS},
  note		= {FTP: waldorf.cs.chalmers.se},
  title		= {Type Theory and Programming},
  year		= {1994}
}

@Article{	  Coquand/Huet88,
  author	= {T. Coquand and G. Huet},
  journal	= {Information and Computation},
  number	= {2/3},
  pages		= {95--120},
  title		= {The {C}alculus of {C}onstructions},
  volume	= {76},
  year		= {1988}
}

@InProceedings{	  Cousot/Cousot77,
  author	= {P. Cousot and R. Cousot},
  title		= {Abstract interpretation: a unified lattice model for
		  static analysis of programs by construction or
		  approximation of fixpoints},
  booktitle	= {Proceedings 4th ACM Symposium Principles of Programming
		  Languages},
  pages		= {238--252},
  year		= {1977}
}

@Article{	  Curzon93a,
  author	= {Paul Curzon},
  title		= {{D}eriving {C}orrectness {P}roperties of {C}ompiled
		  {C}ode},
  journal	= {Formal Methods in System Design},
  volume	= {3},
  pages		= {83--115},
  month		= aug,
  year		= {1993}
}

@Unpublished{	  Curzon94,
  author	= {Paul Curzon},
  title		= {{T}he {V}erified {C}ompilation of {V}ista {P}rograms},
  note		= {Internal Report, Computer Laboratory, University of
		  Cambridge},
  address	= {Cambridge, UK},
  year		= {1994},
  month		= jan
}

@TechReport{	  Cyrluk93,
  author	= {D. Cyrluk},
  title		= {Microprocessor Verification in PVS - A Methodology and
		  Simple Examples.},
  institution	= {SRI International, Computer Science Laboratory},
  year		= {1993},
  number	= {SRI-CSL-93-12},
  month		= {December}
}

@InProceedings{	  Dam86,
  author	= {M. Dam and F. Jensen},
  title		= {Compiler Generation from Relational Semantics},
  booktitle	= {ESOP'86},
  volume	= {213},
  series	= {LNCS},
  year		= {1986},
  publisher	= {Springer-Verlag}
}

@Article{	  Davidson/Fraser80,
  author	= {Davidson, J. W. and Fraser, C. W.},
  title		= {The Design and Application of a Retargetable Peephole
		  Optimizer},
  journal	= {ACM Transactions on Programming Languages and Systems},
  volume	= {2},
  number	= {2},
  month		= apr,
  year		= {1980},
  pages		= {191--202}
}

@InCollection{	  Dershowitz/Jouanaud90,
  author	= {N. Dershowitz and {J.-P.} Jouanaud},
  title		= {Rewrite Systems},
  booktitle	= {Handbook of Theoretical Computer Science, Volume B: Formal
		  Models and Semantics},
  editor	= {J. van Leeuwen},
  publisher	= {Elsevier},
  year		= {1990},
  pages		= {245--320}
}

@PhDThesis{	  Diehl96,
  author	= {Stephan Diehl},
  title		= {{Semantics-Directed Generation of Compilers and Abstract
		  Machines}},
  school	= {University of the Saarland, Germany},
  year		= {1996}
}

@Book{		  Dijkstra76:Disc,
  author	= {Edsger W. Dijkstra},
  title		= {A Discipline of Programming},
  publisher	= {Prentice-Hall},
  year		= {1976}
}

@TechReport{	  Dold+92,
  author	= {A. Dold and {F.W. von} Henke and H. Rue{\ss} and D.
		  Schwier and M. Strecker},
  institution	= {Universit{\"a}t Ulm},
  number	= {93--06},
  title		= {Korso {A}ufgabe: {I}mplementierung von {M}engen mit
		  {H}ilfe von {S}equenzen},
  type		= {Korso Study Note},
  year		= {1993}
}

@TechReport{	  Dold93,
  author	= {A. Dold},
  institution	= {Universit{\"a} Ulm},
  number	= {93--2},
  title		= {Formalisierung {S}chematischer {A}lgorithmen},
  type		= {Korso Study Note},
  year		= {1993}
}

@TechReport{	  Dold94,
  author	= {A. Dold},
  institution	= {Universit{\"a}t Ulm},
  number	= {94-01},
  title		= {Program {D}evelopment with {S}pecification {O}perators},
  type		= {Korso Study Note},
  year		= {1994}
}

@InProceedings{	  Dold95,
  author	= {Axel Dold},
  title		= {{R}epresenting, {V}erifying and {A}pplying {S}oftware
		  {D}evelopment {S}teps using the {PVS} {S}ystem},
  volume	= {936},
  series	= {LNCS},
  pages		= {431--445},
  booktitle	= {Proceedings of the Fourth International Conference on
		  Algebraic Methodology and Software Technology, AMAST'95,
		  Montreal},
  year		= {1995},
  publisher	= {Springer-Verlag},
  editor	= {V.S. Alagar and Maurice Nivat}
}

@InProceedings{	  Drossopoulou+82,
  author	= {Sophia Drossopoulou and Gerhard Goos and Guido Persch and
		  Manfred Dausmann and Georg Winterstein},
  title		= {An Attribute Grammar for Ada},
  year		= {1982},
  volume	= {17:6},
  booktitle	= {Compiler Construction Conference},
  pages		= {334 -- 349}
}

@InProceedings{	  Dybjer85,
  author	= {Dybjer, P.},
  title		= {Using Domain Algebras to prove the correctness of a
		  compiler},
  booktitle	= {2nd Annual Symposium on Theoretical Aspects of Computer
		  Science STACS},
  series	= {LNCS},
  volume	= {182},
  pages		= {98--108},
  year		= {1985}
}

@Book{		  Ehrich:89,
  author	= {H.-D. Ehrich and M. Gogolla and U.W. Lipeck},
  title		= {{Algebraische Spezifikation abstrakter Datentypen}},
  publisher	= {B.G. Teubner},
  year		= {1989}
}

@InProceedings{	  Emmelmann+88,
  author =	 {H. Emmelmann and F.-W. Schr\"oer and R. Landwehr},
  title =	 {BEG - a Generator for Efficient Back Ends},
  booktitle =	 {ACM Proceedings of the Sigplan Conference on
                  Programming Language Design and Implementation},
  month =	 jun,
  year =	 {1989}
}

@InProceedings{	  Emmelmann92,
  author =	 {H. Emmelmann},
  title =	 {Code Selection by regularly controlled term
                  rewriting},
  editor =	 {R. Giegerich and S.L. Graham},
  booktitle =	 {Code Generation - Concepts, Tools, Techniques},
  series =	 {Workshops in Computing},
  publisher =	 {Springer-Verlag},
  year =	 {1992}
}

@PhDThesis{Espinosa95,
  author =	 {David A. Espinosa},
  title =	 {Semantic Lego},
  school =	 {Columbia University},
  year =	 {1995}
}

@InProceedings{	  Farmer+91,
  author =	 {William M. Farmer and Joshua D. Guttman and
                  F. Javier Thayer},
  booktitle =	 {CADE-11},
  publisher =	 {Springer-Verlag},
  series =	 {LNCS},
  volume =	 {607},
  title =	 {Little Theories},
  year =	 {1991}
}

@Article{	  Farmer+93,
  author	= {William M. Farmer and Joshua D. Guttman and F. Javier
		  Thayer},
  journal	= {J. of Automated Reasoning},
  pages		= {213-248},
  title		= {{IMPS}: An Interactive Mathematical Proof System},
  volume	= {11},
  year		= {1993}
}

@Article{	  Fradet+91,
  author	= {P. Fradet and D. Le M\'{e}tayer},
  title		= {{Compilation of Functional Languages by Program
		  Transformation}},
  journal	= {ACM Transactions on Programming Languages and Systems},
  year		= {1991},
  volume	= {13},
  number	= {1},
  pages		= {21--51}
}

@MastersThesis{	  Frank90,
  author	= {Frank, Karsten},
  title		= {{E}ine {g}emeinsame {A}bstrakte {M}aschine {f}\"ur
		  {PROLOG} {u}nd {LISP}},
  school	= {Institut f\"ur Informatik, CAU},
  address	= {{K}iel},
  year		= {1990}
}

@TechReport{	  GMD87,
  author	= {GMD, Forschungsgruppe ``Expertensysteme''},
  title		= {{BABYLON}--{R}eferenzhandbuch {V.} 1.1/1},
  institution	= {Gesellschaft f\"ur Mathematik und Datenverarbeitung (F3)},
  address	= {St. Augustin},
  year		= {1987}
}


@TechReport{	  Gallier92,
  author	= {Jean Gallier},
  address	= {From: ftp.cis.upenn.edu},
  institution	= {University of Pensylvania},
  title		= {Constructive Logics. Part I: A Tutorial on Proof Systems
		  and Typed Lambda-Calculus},
  year		= {1992}
}

@TechReport{	  Garland/Guttag91,
  author	= {{S.J.} Garland and {J.V.} Guttag},
  institution	= {Digital systems Research 'Center},
  number	= {SRC Report 82},
  pages		= {137--151},
  publisher	= {Springer-Verlag},
  title		= {A Guide to LP, The LARCH Prover},
  year		= {1991}
}

@InProceedings{	  Gaudel95,
  author	= {{M.-C.} Gaudel},
  title		= {{A}dvantages and {L}imits of {F}ormal {A}pproaches for
		  {U}ltra-{H}igh {D}ependability},
  booktitle	= {Proc. Predictably Dependable Computing Systems, Esprit
		  Basic Research Series},
  editor	= {B. Randell and {J.-C.} Laprie and H. Kopetz and B.
		  Littlewood},
  publisher	= {Springer-Verlag},
  pages		= {241--252},
  year		= {1995}
}

@Book{		  Gentzen34,
  author	= {Gerhard Gentzen},
  publisher	= {Wissenschaftliche Buchgesellschaft Darmstadt},
  title		= {Untersuchungen \"uber das logische Schlie{\ss}en},
  year		= {1934}
}

@Article{	  Goerigk+96b,
  author	= {Wolfgang Goerigk and Harold Boley and Ulrich Hoffmann and
		  Markus Perling and Michael Sintek},
  title		= {{Komplettkompilation von Lisp: Eine Studie zur
		  \"Ubersetzung von Lisp-Software f\"ur C-Umgebungen}},
  journal	= {KI},
  number	= {2},
  volume	= {10},
  publisher	= {Interdata Verlags GmbH},
  year		= {1996},
  note		= {To appear.}
}

@InProceedings{	  Goerigk/Simon91,
  author	= {Goerigk, W. and Simon, F.},
  title		= {{Z}ielsetzungen im {V}erbundvorhaben {APPLY}},
  booktitle	= {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und
		  Rechner''}},
  address	= {Bericht Nr.\ 8/91-I des Instituts f\"ur angewandte
		  Mathematik und Informatik der Univ.\ M\"unster},
  year		= {1991}
}

@Article{	  Goerigk/Simon93,
  author	= {Goerigk, Wolfgang and Simon, Friedemann},
  title		= {{M}igration und {K}ompilation in {L}isp: {E}in {W}eg von
		  {P}rototypen zu {A}nwendungen},
  journal	= {Proc. Workshop ``Neuere Entwicklungen der deklarativen
		  KI-Programmierung''},
  year		= {1993},
  volume	= {DFKI Research Report RR-93-35},
  pages		= {31-52},
  month		= sep
}

@InProceedings{	  Goerigk89a,
  author	= {Goerigk, W.},
  title		= {Semantik {und \"U}bersetzung {o}bjektorientierter
		  {W}issensrepr\"asentationssprachen},
  booktitle	= {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und
		  Rechner''}},
  address	= {Bad Honnef},
  year		= {1989}
}

@InProceedings{	  Goerigk89b,
  author	= {Goerigk,W.},
  editor	= {Dosch, W.},
  title		= {Zur {K}orrektheit {eines \"U}bersetzers f\"ur
		  {o}bjektorientierte {S}prachen: {E}in {B}eweisansatz},
  booktitle	= {Arbeitstreffen {\em {F}unktionale und logische
		  {P}rogrammierung -- {S}prachen, {M}ethoden,
		  {I}mplementationen}},
  address	= {{I}nstitut f\"ur {M}athematik der {U}niversit\"at
		  {A}ugsburg},
  pages		= {8--20},
  year		= {1989}
}

@PhDThesis{	  Goerigk93,
  author	= {Goerigk, Wolfgang},
  title		= {{K}orrektheit {der \"U}bersetzung {o}bjektorientierter
		  {W}issensrepr\"asentationssprachen {m}it {s}tatischer
		  {V}ererbung},
  school	= {Math.-Nat. Fakult\"at der
		  Christian-Albrechts-Universit\"at zu Kiel},
  address	= {{K}iel},
  year		= {1993}
}

@InProceedings{	  Goerigk95,
  author	= {Wolfgang Goerigk},
  title		= {{O}n the {C}orrectness of {C}ompilers and {C}ompiler
		  {I}mplementations},
  booktitle	= {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und
		  Rechner''}},
  address	= {Bad Honnef},
  year		= {1995}
}

@Book{		  Goldberg/Robson83,
  author	= {Goldberg, A. and Robson, D.},
  title		= {Smalltalk--80: The {L}anguage and its {I}mplementation},
  publisher	= {Addison--Wesley},
  address	= {Reading, MA},
  year		= {1983}
}


@Article{	  Goodenough/Gerhart75,
  author	= {{J.B.} Goodenough and {S.L.} Gerhart},
  title		= {{T}oward a {T}heory of {T}est {D}ata {S}election},
  journal	= {SIGPLAN Notices},
  number	= {6},
  volume	= {10},
  month		= jun,
  pages		= {493--510},
  year		= {1975}
}

@Article{	  Goos/Winterstein80,
  author	= {Gerhard Goos and Georg Winterstein},
  title		= {Towards a Compiler Front-End for Preliminary Ada},
  year		= {1980},
  journal	= {SIGPLAN Notices},
  volume	= {15},
  number	= {11},
  pages		= {36 -- 46}
}

@Article{	  Goos81,
  author	= {Gerhard Goos},
  title		= {Problems in Compiling Ada},
  year		= {1981},
  journal	= {LNCS},
  volume	= {123},
  pages		= {173 -- 199}
}

@InProceedings{	  Grosch/Emmelmann90,
  author	= {J. Grosch and H. Emmelmann},
  title		= {A Tool Box for Compiler Construction},
  booktitle	= {Compiler Compilers, Third International Workshop, CC'90;
		  Schwerin, FRG; Proceedings},
  year		= {1990},
  series	= {LNCS},
  volume	= {477},
  publisher	= {Springer-Verlag}
}

@InCollection{	  Gunter/Scott90,
  key		= {Gunter \& Scott},
  author	= {C. A. Gunter and D. S. Scott},
  title		= {Semantic Domains},
  booktitle	= {Handbook of Theoretical Computer Science},
  chapter	= {8},
  pages		= {633--674},
  volume	= {B: Formal Models and Semantics},
  editor	= {J. van Leeuwen},
  publisher	= {North-Holland},
  address	= {New York, N.Y.},
  year		= {1990},
  annote	= {24 references.}
}

@InProceedings{	  Gurevich-Huggins93,
  author	= {Y. Gurevich and J. Huggins},
  title		= {{T}he {S}emantics of the {C} {P}rogramming {L}anguage},
  volume	= {702},
  series	= {LNCS},
  pages		= {274--308},
  booktitle	= {{CSL} '92},
  publisher	= {Springer-Verlag},
  year		= {1993}
}

@Article{	  Gurevich91,
  author	= {Y. Gurevich},
  title		= {{E}volving {A}lgebras; {A} {T}utorial {I}ntroduction},
  journal	= {Bulletin EATCS},
  year		= {1991},
  volume	= {43},
  pages		= {264--284}
}

@InCollection{Gurevich93,
  author =       "Yuri Gurevich",
  title =        "Evolving Algebras: An Attempt to Discover Semantics",
  booktitle =    "Current Trends in Theoretical Computer Science",
  publisher =    "World Scientific",
  year =         "1993",
  editor =       "G. Rozenberg and A. Salomaa",
  pages =        "266--292",
  address =      "River Edge, NJ",
}

@InProceedings{Gurevich95,
  author	= {Y. Gurevich},
  title		= {{E}volving {A}lgebras: {L}ipari {G}uide},
  editor	= {E. B\"orger},
  booktitle	= {Specification and Validation Methods},
  publisher	= {Oxford University Press},
  year		= {1995}
}

@TechReport{Gurevich97,
  author	= {Y. Gurevich},
  title		= {{May 1997 Draft on the ASM Guide}},
  institution	= {EECS Dept., University of Michigan},
  year		= {1997}
}

@TechReport{	  Guttman+92,
  author	= {{J. D.} Guttman and {L. G.} Monk and {J. D.} Ramsdell and
		  {W. M.} Farmer and V. Swarup},
  title		= {{A} {G}uide to {VLisp}, {A} {V}erified {P}rogramming
		  {L}anguage {I}mplementation},
  institution	= {The MITRE Corporation},
  type		= {Technical Report},
  number	= {M92B091},
  address	= {Bedford, MA},
  month		= sep,
  year		= {1992}
}

@PhDThesis{	  Habel92,
  author	= {Annegret Habel},
  title		= {Hyperedge Replacement: Grammars and Languages},
  school	= {{Universit\"at Bremen}},
  year		= {1992},
  note		= {Springer-Verlag. LNCS 643}
}

@InProceedings{	  Hannan/Pfenning92,
  author	= {John Hannan and Frank Pfenning},
  address	= {Santa Cruz, California},
  booktitle	= {Seventh Annual {IEEE} Symposium on Logic in Computer
		  Science},
  key		= {Hannan92},
  month		= jun,
  note		= {Preliminary version available as {POP} Report 91--003,
		  School of Computer Science, Carnegie Mellon University},
  pages		= {407--417},
  publisher	= {IEEE Computer Society Press},
  title		= {Compiler Verification in {LF}},
  year		= {1992}
}

@Article{	  Hannan:1994,
  author	= {John Hannan},
  title		= {Operational Semantics-Directed Compilers and Machine
		  Architectures},
  journal	= {ACM Transactions on Programming Languages and Systems},
  volume	= {16},
  number	= {4},
  pages		= {1215--1247},
  month		= {jul},
  year		= {1994},
  coden		= {ATPSDT},
  issn		= {0164-0925},
  url		= {http://www.acm.org/pubs/toc/Abstracts/0164-0925/183458.html}
		  ,
  keywords	= {languages; theory}
}

@Article{	  Hannan:1994:OSD,
  author	= {John Hannan},
  title		= {Operational Semantics-Directed Compilers and Machine
		  Architectures},
  journal	= {ACM Transactions on Programming Languages and Systems},
  volume	= {16},
  number	= {4},
  pages		= {1215--1247},
  month		= jul,
  year		= {1994},
  issn		= {0164-0925},
  abstract	= {We consider the task of automatically constructing
		  intermediate-level machine architectures and compilers
		  generating code for these architectures, given operational
		  semantics for source languages. We use operational
		  semantics in the form of abstract machines given by rewrite
		  systems in which the rewrite rules operate on terms
		  representing states of computations. To construct compilers
		  and new architectures we employ a particular strategy
		  called pass separation, a form of staging transformation,
		  that takes a program $p$ and constructs a pair of programs
		  $p_{1}, p_{2}$ such that $p(x, y) = p_{2}(p_{1}(x), y)$ for
		  all $x,y$. If $p$ represents an operational semantics for a
		  language, with arguments $x$ and $y$ denoting a source
		  program and its input data, then pass separation constructs
		  programs $p_{1}$ and $p_{2}$ corresponding to a compiler
		  and an executor. \par The compiler translates the source
		  language into an intermediate-level target language, and
		  the executor provides the definition for this language. Our
		  use of pass separation supports the automatic definition of
		  target languages or architectures, and the structure of
		  these architectures is directed by the structure of the
		  given source semantics. These architectures resemble
		  abstract machine languages found in hand-crafted compilers.
		  Our method is restricted to a limited class of abstract
		  machines given as term-rewriting systems, but we argue that
		  this class encompasses a large set of language definitions
		  derived from more natural operational semantics. We provide
		  two examples of our method by constructing compilers and
		  target architectures for a simple functional language and a
		  simple imperative language. Though we construct these
		  architectures automatically, they bear a striking
		  resemblance to existing architectures constructed by hand.}
}

@Article{	  HannanJohn1992a,
  author	= {John Hannan and Dale Miller},
  title		= {From Operational Semantics to Abstract Machines},
  year		= {1992},
  number	= {4},
  pages		= {415--459},
  volume	= {2},
  journal	= {Journal of Mathematical Structures in Computer Science}
}

@InProceedings{	  Hennessey92,
  author	= {Hennessey, W.},
  title		= {{WCL}: {D}elivering {E}fficient {C}ommon {L}isp
		  {A}pplications under {U}nix},
  booktitle	= {Proc. of the 1992 ACM Conference on Lisp and Functional
		  Programming},
  pages		= {260-269},
  address	= {San Francisco, CA},
  year		= {1992}
}

@Article{	  Hoare+93,
  author	= {{C.A.R.} Hoare and He Jifeng and A. Sampaio},
  title		= {{N}ormal {F}orm {A}pproach to {C}ompiler {D}esign},
  journal	= {Acta Informatica},
  volume	= {30},
  pages		= {701--739},
  year		= {1993}
}

@Article{	  Hoare/Lauer74,
  author	= {{C.A.R.} Hoare and {P.E.} Lauer},
  title		= {Consistent and Complementary Formal Theories of the
		  Semantics of Programming Languages},
  journal	= {Acta Informatica},
  year		= {1974},
  volume	= {3},
  pages		= {135-154}
}

@Article{	  Hoare69,
  author	= {C. A. R. Hoare},
  title		= {An axiomatic basis for computer programming},
  journal	= {Communications of the ACM},
  volume	= {12},
  pages		= {576--583},
  year		= {1969}
}

@InProceedings{	  Hoare91,
  author	= {C. A. R. Hoare},
  title		= {Refinement algebra proves correctness of compiling
		  specifications},
  editor	= {{C.C.} Morgan and {J.C.P.} Woodcock},
  booktitle	= {3rd Refinement Workshop},
  publisher	= {Springer-Verlag},
  pages		= {33--48},
  year		= {1991}
}

@Manual{	  Huet+93,
  author	= {G. {Huet et al.}},
  edition	= {5.8},
  key		= {Coq93},
  month		= nov,
  note		= {FTP: von ftp.inria.fr},
  organization	= {INRIA-Rocquencourt},
  title		= {The {Coq} Proof Assistant, User's Guide},
  year		= {1993}
}

@Article{HugVan98,
  author =       {J. Huggins and D. {Van Campenhout}},
  title =        {{Specification and Verification of Pipelining in the
                  ARM2 RISC Microprocessor}},
  journal =      {{ACM Transactions on Design Automation of Electronic 
                   Systems}}, 
  year =         {1998},
  volume =       {3},
  number =       {4},
  month =        {October},
  pages =        {563--580}
}



@Manual{	  Inmos88,
  title		= {Transputer instruction set: {A} compiler writer's guide},
  publisher	= {Prentice Hall},
  organization	= {Inmos Limited},
  year		= {1988}
}

@Article{	  JACM::WassermanB1997,
  title		= {Software Reliability via Run-Time Result-Checking},
  author	= {Hal Wasserman and Manuel Blum},
  area		= {Formal Languages and Complexity Theory},
  journal	= {Journal of the ACM},
  pages		= {826--849},
  month		= nov,
  year		= {1997},
  volume	= {44},
  number	= {6},
  keywords	= {algorithms, reliability, verification, Built-in testing,
		  concurrent error detection, debugging, fault tolerance,
		  Fourier Transform, result-checking, self-correcting},
  general-terms	= {Reliability, Algorithms, Verification},
  cr-categories	= {D.2.5; F.2.1[Computation of transforms]; F.3.1},
  preliminary	= {focs::BlumW1994:382},
  abstract	= {We review the field of result-checking, discussing simple
		  checkers and self-correctors. We argue that such checkers
		  could profitably be incorporated in software as an aid to
		  efficient debugging and enhanced reliability. We consider
		  how to modify traditional checking methodologies to make
		  them more appropriate for use in real-time, real-number
		  computer systems. In particular, we suggest that checkers
		  should be allowed to use stored randomness: that is, that
		  they should be allowed to generate, preprocess, and store
		  random bits prior to run-time, and then to use this
		  information repeatedly in a series of run-time checks. In a
		  case study of checking a general real-number linear
		  transformation (e.g., a Fourier Transform), we present a
		  simple checker which uses stored randomness, and a
		  self-corrector which is particularly efficient if stored
		  randomness is employed.},
  subject	= {{\bf D.2.5} Software, SOFTWARE ENGINEERING, Testing and
		  Debugging. {\bf F.2.1} Theory of Computation, ANALYSIS OF
		  ALGORITHMS AND PROBLEM COMPLEXITY, Numerical Algorithms and
		  Problems, Computation of transforms. {\bf F.3.1} Theory of
		  Computation, LOGICS AND MEANINGS OF PROGRAMS, Specifying
		  and Verifying and Reasoning about Programs.},
  references	= {\cite{STOC::ArBCG1993} \cite{FOCS::AroraS1992}
		  \cite{FOCS::AroraS1992} \cite{CC::babaiFL1991}
		  \cite{STOC::babaiFLS1991} \cite{STACS::BeaverF1990}
		  \cite{CC::BeigelF1992} \cite{ALGOR::BlumEGKN1994}
		  \cite{STOC::blumK1989} \cite{JCSS::blumLR1993}
		  \cite{IEEETSE::ButlerF1993} \cite{STOC::Ergun1995}
		  \cite{IPL::FortnowS1988} \cite{MFCS::Freivalds1979}
		  \cite{STOC::GemmellLRSW1991} \cite{IPL::GemmellS1992}
		  \cite{FOCS::GoldreichMW1986} \cite{STACS::Lipton1990}
		  \cite{JACM::LundFKN1992} \cite{IPL::Rubinfeld1992}
		  \cite{FOCS::Rubinfeld1994} \cite{SODA::RubinfeldS1992}
		  \cite{SICOMP::RubinfeldS1996} \cite{JACM::Schwartz1980}
		  \cite{FOCS::Shamir1990} \cite{TCS::Valiant1979}
		  \cite{JCSS::WegmanC1981} \cite{STOC::Yao1990}}
}

%%% doppelt: (!)
@Article{	  JACM:WassermanBlum:1997,
  title		= {Software Reliability via Run-Time Result-Checking},
  author	= {Hal Wasserman and Manuel Blum},
  area		= {Formal Languages and Complexity Theory},
  journal	= {Journal of the ACM},
  pages		= {826--849},
  month		= nov,
  year		= 1997,
  volume	= 44,
  number	= 6
}

@InProceedings{	 Jacobs+98,
  author =	 {B. Jacobs and J. van den Berg and M. Huisman and
                  M. van Berkumand U. Hensel, H. Tews},
  title =	 {Reasoning about Java Classes (Preliminary Report)},
  booktitle =	 {Proceedings of Object-Oriented Programming Systems,
                  Languages and Applications (OOPSLA'98)},
  year =	 1998
}

@Article{	  Janssen98,
  author	= {T.M.V. Janssen},
  title		= {Algebraic Translations, Correctness and Algebraic Compiler
		  Construction},
  journal	= {Theoretical Computer Science},
  year		= {1998},
  volume	= {199},
  pages		= {25--56}
}

@Book{		  Jensen-Wirth:Pascal75,
  author	= {K. Jensen and N. Wirth},
  title		= {{PASCAL} {U}ser {M}anual and {R}eport},
  publisher	= {Springer-Verlag},
  year		= {1975}
}

@InProceedings{	  Jones/Schmidt80,
  author	= {Jones, {N. D.} and Schmidt, {D. A.}},
  title		= {Compiler generation from denotational semantics},
  series	= {LNCS},
  volume	= {94},
  booktitle	= {Workshop on Semantics Directed Compiler Generation},
  year		= {1980}
}

@Book{		  Jones90,
  author	= {C. B. Jones},
  title		= {{Systematic Software Development Using VDM, 2nd ed.}},
  publisher	= {Prentice Hall},
  address	= {New York, London},
  year		= {1990}
}

@TechReport{	  Joyce89,
  author	= {J.J. Joyce},
  address	= {New Museums Site, Pembroke Street, Cambridge, CB2 3QG,
		  England},
  institution	= {University of Cambridge},
  month		= mar,
  number	= {167},
  title		= {A verified compiler for a Verified Microprocessor},
  year		= {1989}
}

@InProceedings{	  Joyce90,
  author	= {Joyce, {Jeffrey J.}},
  title		= {Totally {V}erified {S}ystems: {L}inking {V}erified
		  {S}oftware to {V}erified {H}ardware},
  editor	= {Leeser, M. and Brown, G.},
  series	= {LNCS},
  volume	= {408},
  booktitle	= {Hardware Specification, Verification and Synthesis:
		  Mathematical Aspects},
  year		= {1990}
}

@Article{	  KP97,
  author	= {P. W. Kutter and A. Pierantonio},
  title		= {Montages Specifications of Realistic Programming
		  Languages},
  journal	= {Journal of Universal Computer Science},
  year		= {1997},
  volume	= {3},
  number	= {5},
  pages		= {416--442}
}

@InProceedings{	  Kamin88,
  author	= {Kamin, S.},
  title		= {{I}nheritance in {S}malltalk--80: {A} {D}enotational
		  {A}pproach},
  booktitle	= {Proceedings of POPL},
  pages		= {80--87},
  organization	= {ACM},
  year		= {1988}
}

@TechReport{	  Karger92,
  author	= {{Burghard v.} Karger},
  title		= {{D}istinguishing {D}ivergence from {C}haos in {CSP}},
  type		= {ProCoS Report},
  institution	= {Universit\"at Kiel},
  year		= {1992}
}

@TechReport{	  Karger93,
  author	= {{Burghard v.} Karger},
  title		= {{A}lgebraic {C}ompiler {V}erification},
  type		= {Internal Report},
  institution	= {Oxford University Computing Laboratory},
  month		= oct,
  year		= {1993}
}

@Article{	  Kastens80,
  author	= {U. Kastens},
  title		= {Ordered Attribute Grammars},
  journal	= {Acta Informatica},
  volume	= {13},
  number	= {3},
  year		= {1980},
  pages		= {229--256}
}

@TechReport{	  Kaufmann/Moore94,
  author	= {M. Kaufmann and {J S.} Moore},
  title		= {{Design Goals of ACL2}},
  institution	= {Computational Logic, Inc.},
  type		= {Technical Report},
  number	= {101},
  month		= aug,
  year		= {1994}
}

@Book{		  Keene89,
  author	= {Keene, {S.E.}},
  title		= {Object {O}riented {P}rogramming in {Common Lisp}},
  publisher	= {Addison--Wesley},
  address	= {Reading, MA},
  year		= {1989}
}

@PhDThesis{	  Kelsey89,
  author	= {Richard A. Kelsey},
  title		= {{Compilation by Program Transformation}},
  school	= {Yale University},
  year		= {1989}
}

@Book{		  Kernighan/Ritchie78,
  author	= {Kernighan, {B.W.} and Ritchie, {D.M.}},
  title		= {{T}he {C} {P}rogramming {L}anguage},
  publisher	= {Prentice-Hall},
  address	= {Englewoods Cliff, NY},
  year		= {1978}
}

@Book{		  Kernighan/Ritchie83,
  author	= {Kernighan, {B.W.} and Ritchie, {D.M.}},
  title		= {{P}rogrammieren in {C}},
  publisher	= {Hanser Verlag},
  address	= {M\"unchen, Wien},
  year		= {1983}
}

@Book{		  Kersten95,
  author	= {H. Kersten},
  title		= {{S}icherheit in der {I}nformationstechnik, 2. {A}ufl.},
  publisher	= {Oldenbourg},
  year		= {1995},
  address	= {M\"unchen, Wien}
}

@InProceedings{	  Knemeyer/Schulenburg93,
  author	= {Knemeyer, U. and {Graf von der Schulenburg}, {J.-M.}},
  editor	= {Puppe, F. and G\"unter, A.},
  title		= {``{E}xpertensysteme'' - {W}elche {F}aktoren f\"ordern und
		  hemmen die {I}mplementation und {D}iffusion der
		  {T}echnologie in der {V}ersicherungswirtschaft.},
  booktitle	= {Expertensysteme '93},
  publisher	= {Informatik aktuell, Springer-Verlag},
  address	= {Berlin, Heidelberg, New York},
  year		= {1993}
}

@InProceedings{	  Knoop+92,
  author	= {Knoop, J. and R\"uthing, O. and Steffen, B.},
  address	= {San Francisco, CA},
  booktitle	= {Proc.~{ACM SIGPLAN} Conference on Programming Language
		  Design and Implementation'92},
  pages		= {224 - 234},
  series	= {{ACM SIGPLAN} Notices},
  volume	= {{\em 27},7},
  title		= {Lazy code motion},
  month		= jun,
  year		= {1992}
}

@Unpublished{	  Knoop+93a,
  author	= {Knoop, J. and R\"uthing, O. and Steffen, B.},
  note		= {To appear in ~ACM Transactions on Programming Languages
		  and Systems. Available as MIP-Bericht 9310, Fakult\"at
		  f\"ur Mathematik und Informatik, Universit\"at Passau, 35
		  pages},
  title		= {Optimal Code Motion: {T}heory and Practice},
  year		= {1993}
}

@Article{	  Knoop+93b,
  author	= {Knoop, J. and R\"uthing, O. and Steffen, B.},
  journal	= {Journal of Programming Languages},
  title		= {Lazy Strength Reduction},
  year		= {1993},
  volume	= {1},
  number	= {1},
  pages		= {71-91},
  publisher	= {Chapman \& Hall},
  address	= {London, UK}
}

@InProceedings{	  Knoop+94,
  author	= {Knoop, J. and R\"uthing, O. and Steffen, B.},
  title		= {Partial Dead Code Elimination},
  booktitle	= {Proc.~{ACM SIGPLAN} Conference on Programming Language
		  Design and Implementation'94},
  address	= {Orlando, FL},
  month		= jun,
  year		= {1994},
  note		= {To appear}
}

@InProceedings{	  Knoop/Steffen92a,
  author	= {Knoop, J. and Steffen, B.},
  address	= {Paderborn, Germany},
  booktitle	= {Proc. 4$^{th}$~Conference on Compiler Construction (CC)},
  pages		= {125 - 140},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  volume	= {641},
  title		= {The Interprocedural Coincidence Theorem},
  year		= {1992}
}

@InProceedings{	  Knoop/Steffen92b,
  author	= {Knoop, J. and Steffen, B.},
  address	= {Paderborn, Germany},
  booktitle	= {Addenda to Proc. 4$^{th}$~Conference on Compiler
		  Construction (CC)},
  pages		= {36 - 39},
  publisher	= {Published as Tech. Rep. No. 103, Department of Computer
		  Science, University of Paderborn},
  title		= {Optimal interprocedural partial redundancy elimination.
		  {E}xtended abstract},
  year		= {1992}
}

@InProceedings{	  Knoop/Steffen92c,
  author	= {Knoop, J. and Steffen, B.},
  address	= {Schlo{\ss} Dagstuhl, Germany},
  booktitle	= {Software Construction---Foundation and Application},
  editor	= {Langmaack, H. and Neuhold, E. and Paul, M.},
  organization	= {Internationales Begegnungs- und Forschungszentrum f\"ur
		  Informatik},
  series	= {Dagstuhl-Seminar-Report 29},
  title		= {Optimal Interprocedural Data Flow Analysis},
  year		= {1992}
}

@PhDThesis{	  Knoop93,
  author	= {Knoop, J.},
  title		= {Optimal Interprocedural Program Optimization: {A} new
		  framework and its application},
  school	= {Institut f\"ur Informatik, CAU},
  year		= {1993},
  note		= {To appear as monograph in the series {\em Lecture Notes in
		  Computer Science}, Springer-Verlag, Heidelberg, Germany,
		  1994.}
}

@Unpublished{	  Knoop94,
  author	= {Knoop, J.},
  title		= {Higher Order Data Flow Analysis},
  note		= {Submitted to the {\em IFIP Working Conference on
		  ``Programming Concepts, Methods and Calculi
		  (PROCOMET'94)''}},
  month		= jun,
  year		= {1994},
  address	= {San Miniato, Italy}
}

@MastersThesis{	  Knutzen91,
  author	= {Knutzen, Heinz},
  title		= {{C}odegenerierung und {L}aufzeitsystem {e}ines {C}ompilers
		  {v}on {Common Lisp} {n}ach {C}},
  school	= {Institut f\"ur Informatik, CAU},
  address	= {{K}iel},
  year		= {1991}
}

@Book{		  Kock92,
  author	= {G. Kock},
  title		= {Spezifikation und Verifikation von
		  Optimierungsalgorithmen},
  note		= {Dissertation an der Universit\"at Karlsruhe},
  publisher	= {Oldenburg Verlag},
  year		= {1992}
}

@InProceedings{	  Landwehr+82,
  author	= {Rudolf Landwehr and H.-St. Jansohn and Gerhard Goos},
  title		= {Experience with an Automatic Code Generator Generator},
  year		= {1982},
  volume	= {17:6},
  booktitle	= {Compiler Construction Conference},
  pages		= {56 -- 66}
}

@Misc{		  Langmaack/Goerigk95,
  author	= {Hans Langmaack and Wolfgang Goerigk},
  title		= {{Technik verifizierter \"U}bersetzerimplementierung ({{\em
		  {VerComp}\/}})},
  year		= {1995},
  address	= {Kiel},
  howpublished	= {DFG-Projektantrag. Kiel}
}

@TechReport{	  Langmaack89,
  author	= {Langmaack, H.},
  title		= {{\"U}ber {v}ollst\"andig {o}perationell {a}d\"aquate
		  {d}enotationelle {S}emantik {f}unktionaler
		  {P}rogrammiersprachen},
  institution	= {Institut f\"ur Informatik, CAU},
  type		= {Institutsbericht},
  number	= {Nr. 8901},
  address	= {Kiel},
  year		= {1989}
}

@Book{		  Lee89,
  author	= {P. Lee},
  title		= {Realistic Compiler Generation},
  publisher	= {MIT Press},
  year		= {1989}
}

@Book{		  Lippe/Simon90,
  author	= {Lippe, W. and Simon, F.},
  title		= {{A}pplikative {P}rogrammierung},
  publisher	= {Lehrbuch, Springer-Verlag},
  address	= {Berlin},
  year		= {In Vorbereitung}
}

@InProceedings{	  Littlewood/Strigini95,
  author	= {B. Littlewood and L. Strigini},
  title		= {{V}alidation of {U}ltra-{H}igh {D}ependability for
		  {S}oftware-based {S}ystems},
  booktitle	= {Proc. Predictably Dependable Computing Systems, Esprit
		  Basic Research Series},
  editor	= {B. Randell and {J.-C.} Laprie and H. Kopetz and B.
		  Littlewood},
  publisher	= {Springer-Verlag},
  pages		= {473--494},
  year		= {1995}
}

@Book{		  Loeckx-Sieber,
  author	= {J. Loeckx and K. Sieber},
  title		= {{The Foundations of Program Verification (Second
		  edition)}},
  publisher	= {John Wiley and Sons},
  address	= {New York},
  year		= {1987}
}

@Book{		  Loeckx:96,
  author	= {J. Loeckx and H.-D. Ehrich and M. Wolf},
  title		= {{Specification of Abstract Data Types}},
  publisher	= {{John Wiley \& Sons Ltd.} and {B.G. Teubner}},
  year		= {1996}
}

@Manual{	  Luo/Pollack92,
  author	= {Z. Luo and R. Pollack},
  month		= may,
  organization	= {University of Edinburgh},
  title		= {{LEGO} Proof Development System: User's Manual},
  year		= {1992}
}

@TechReport{	  Luo90,
  author	= {Z. Luo},
  institution	= {University of Edinburgh},
  month		= jul,
  number	= {CST-65-90},
  title		= {An {E}xtended {C}alculus of {C}onstructions},
  year		= {1990}
}

@Article{	  Luo91a,
  author	= {Z. Luo},
  journal	= {Information and Computation},
  pages		= {107--137},
  title		= {A {H}igher-{O}rder {C}alculus and {T}heory {A}bstraction},
  volume	= {90},
  year		= {1991}
}

@InProceedings{	  Luo91b,
  author	= {Z. Luo},
  booktitle	= {TAPSOFT'91},
  editor	= {S. Abramsky and T.S.E. Maibaum},
  pages		= {143--168},
  publisher	= {Springer-Verlag},
  title		= {Program Specification and Data Refinement in Type Theory},
  year		= {1991}
}

@Article{	  Marriott93,
  author	= {K. Marriott},
  title		= {Frameworks for abstract interpretation},
  journal	= {Acta Informatica},
  volume	= {30},
  pages		= {103--129},
  year		= {1993}
}

@InProceedings{	  McCarthy/Painter67,
  author	= {McCarthy, J. and Painter, {J.A.}},
  title		= {Correctness of a Compiler for Arithmetical Expressions},
  editor	= {J.T. Schwartz},
  booktitle	= {Proceedings of a Symposium in Applied Mathematics, 19,
		  Mathematical Aspects of Computer Science},
  organization	= {American Mathematical Society},
  year		= {1967}
}

@InProceedings{	  McCarthy60,
  author	= {McCarthy, J.},
  title		= {{R}ecursive {F}unctions of {S}ymbolic {E}xpressions and
		  their {C}omputation by {M}achine, {P}art {I}},
  booktitle	= {Communications of the ACM},
  series	= {Vol. 3},
  number	= {4},
  year		= {1960}
}

@Book{		  McCarthy62,
  author	= {McCarthy, J. and Abrahams, {P.W.} and Edwards, {D.J.} and
		  Hart, {T.P.} and Levin, {M.I.}},
  title		= {LISP 1.5 {P}rogrammer's {M}anual},
  publisher	= {The MIT Press},
  address	= {Cambridge, MA},
  year		= {1962}
}

@PhDThesis{	  Meijer92,
  author	= {E. Meijer},
  title		= {Calculating Compilers},
  school	= {University of Nijmwegen},
  year		= {1992}
}

@Book{		  Mertens+93,
  author	= {Mertens, P. and Barowski,V. and Geis, W.},
  title		= {{B}etriebliche {E}xpertensystem-{A}nwendungen},
  publisher	= {2. Auflage, Springer-Verlag},
  address	= {Berlin, Heidelberg, New York},
  year		= {1990}
}

@Book{		  Milner+90,
  author	= {Robin Milner and Mads Tofte and Robert Harper},
  title		= {{T}he {D}efinition of {S}tandard {ML}},
  publisher	= {MIT Press},
  year		= {1990}
}

@MastersThesis{	  Mohnberg90,
  author	= {Mohnberg, A.},
  title		= {{G}arbage {C}ollection {f}\"ur {COLIBRI}, {A}nforderungen,
		  {K}onzepte {u}nd {I}mplementierung},
  school	= {Institut f\"ur Informatik, CAU},
  address	= {{K}iel},
  year		= {1990}
}

@TechReport{	  Montages97,
  author	= {A. Pierantonio and P. W. Kutter},
  title		= {Montages: Towards the Semantics of Realistic Programming
		  Languages},
  institution	= {Dip. Matematica Pura ed Applicata, Università di
		  L'Aquila},
  type		= {techreport},
  number	= {126/Jan},
  month		= jan,
  year		= {1997},
  url		= {http://univaq.it/~alfonso/montages/papers/TR-126.ps.gz},
  seealsourl	= {http://univaq.it/~alfonso/montages/Mhome.html},
  note		= {Presents a case study of Oberon},
  abstract	= {We present a mathematical instrument called Montages for
		  the formal semantic description of realistic, full--scale
		  programming languages. Montages specificat ions are modular
		  and their structure guides the design process. Syntax,
		  static and dynamic semantics are described in a unified
		  setting by means of visual and textual specification
		  elements. The formalism is based on Gurevich's Abstract
		  State Machines and can be equally well understood by
		  language designers, compiler constructors, and programmers.
		  Ease of specification, abstractness, compactness, and
		  intuitivity make Montages suitable for the entire language
		  life cycle, including documentation by language manuals.
		  Compared with traditional manuals, Montages are similar in
		  structure, length, and complexity, but with a formal
		  semantics.}
}

@InProceedings{	  Moore/Kaufmann96,
  author	= {{J S.} Moore and M. Kaufmann},
  title		= {{ACL2}: {A}n Industrial Strength Version of {Nqthm}},
  booktitle	= {Proceedings of COMPASS '96},
  year		= {1996},
  month		= jun
}

@TechReport{	  Moore88,
  author	= {{J S.} Moore},
  address	= {Austin, Texas},
  institution	= {Comp. Logic Inc},
  number	= {22},
  title		= {Piton: A Verified Assembly Level Language},
  year		= {1988}
}

@Article{	  Moore89,
  author	= {{J S.} Moore},
  title		= {A mechanically verified language implementation},
  journal	= {Journal of Automated Reasoning},
  year		= {1989},
  volume	= {5},
  number	= {4}
}

@Article{	  Moore89a,
  key		= {Moore},
  author	= {J. Strother Moore},
  title		= {System verification},
  journal	= {Journal of Automated Reasoning},
  pages		= {409--410},
  volume	= {5},
  number	= {4},
  month		= dec,
  year		= {1989},
  location	= {CMU E\&{}S Library}
}

@TechReport{	  Moore92,
  author	= {{J S.} Moore},
  address	= {Austin, Texas},
  institution	= {Lecture Res. Prog. Pres., Comp. Logic Inc.},
  title		= {{T}he {A}cl2-{P}roject},
  year		= {1992}
}

@Book{		  Moore96,
  author	= {J S. Moore},
  title		= {Piton, A Mechanically Verified Assembly-Level Language},
  publisher	= {Kluwer Academic Publishers},
  year		= {1996}
}

@InProceedings{	  Morris74,
  author	= {{F. L.} Morris},
  title		= {Advice on structuring compilers and proving them correct},
  booktitle	= {1st Proceedings of Principles of Programming Languages},
  pages		= {144--152},
  year		= {1974}
}

@TechReport{	  Mosses79,
  author	= {P. D. Mosses},
  title		= {SIS - semantics implementation system, reference manual
		  and user guide},
  number	= {Departmental Report DAIMI MD-30},
  institution	= {Computer Science Department, Aarhus University},
  year		= {1979}
}

@InProceedings{	  Mosses82,
  author	= {P. D. Mosses},
  title		= {Abstract semantic algebras},
  booktitle	= {Formal description of programming concepts II},
  organization	= {IFIP IC-2 Working Conference},
  editor	= {D. Bj{\o}rner},
  publisher	= {North Holland},
  pages		= {63--88},
  year		= {1982}
}

@Book{		  Mosses92,
  author	= {P. D. Mosses},
  title		= {Action Semantics},
  publisher	= {Cambridge University Press},
  year		= {1992}
}

@PhDThesis{	  mueller:95:diss,
  author	= "Thomas M{\"u}ller",
  title		= "Effiziente Verfahren zur Befehlsanordung",
  year		= "1995",
  month		= jun,
  school	= {Universit{\"a}t Karlsruhe, Fakult{\"a}t f{\"u}r Informatik}
}

@MastersThesis{	  Mueller-Olm90,
  author	= {Markus M\"uller-Olm},
  title		= {{Korrektheit einer \"Ubersetzung der Sprache rekursiver
		  Funktionsdefinitionen erster Ordnung in eine einfache
		  imperative Sprache}},
  school	= {CAU Kiel},
  year		= {1990}
}

@InCollection{	  Mueller-Olm93,
  author	= {Markus M\"uller-Olm},
  title		= {{P}roven {C}orrect {C}ompiling {S}pecification {SubLisp}
		  to {PL}},
  booktitle	= {{P}rovably {C}orrect {S}ystems},
  publisher	= {ProCos I Partners},
  year		= {1993},
  chapter	= {30},
  editor	= {Dines Bj\o rner and Hans Langmaack and C.~A.~R.~Hoare},
  pages		= {405--451}
}

@TechReport{	  Mueller-Olm95,
  author	= {Markus M\"uller-Olm},
  title		= {{A}n {E}xercise in {C}ompiler {V}erification},
  type		= {Internal Report},
  institution	= {CS Department, University of Kiel},
  year		= {1995}
}

@Book{		  Nagl90,
  author	= {M. Nagl},
  title		= {{Softwaretechnik: Methodisches Programmieren im Gro\ss
		  en}},
  publisher	= {Springer-Verlag},
  address	= {Berlin, Heidelberg},
  year		= {1990}
}

@Book{		  Nagl91,
  author	= {M. Nagl},
  title		= {{ADA, Eine Einf\"uhrung in die Programmiersprache der
		  Softwaretechnik}},
  publisher	= {Vieweg-Verlag},
  year		= {1991},
  edition	= {3.\ verb.\ }
}

@InProceedings{	  NeculaLee:98,
  author	= {G. C. Necula and P. Lee},
  title		= {The Design and Implementation of a Certifying Compiler},
  year		= {1998},
  annote	= {appeared also as SIGPLAN notices Vol 33 Number 5,May 1998.
		  url: http://www.cs.cmu.edu/~necula/pldi98.ps.gz},
  pages		= {333--344},
  abstract	= {This paper presents a compiler from a type-safe subset of
		  the C language to optimized DEC Alpha machine code. The
		  novel feature of the compiler is that it contains a
		  certifier that automatically checks the type safety and
		  memory safety of any assembly language program produced by
		  the compiler. The result of the certifier is either a
		  formal proof of type safety or a counterexample pointing to
		  a potential violation of the type system by the
		  assembly-language target program. The ensemble of the
		  compiler and the certifier is called a certifying compiler.
		  Several advantages of certifying compilation over previous
		  approaches can be claimed. The notion of a certifying
		  compiler is significantly easier to employ than a formal
		  compiler verification, in part because it is generally
		  easier to verify the correctness of the result of a
		  computation than to prove the correctness of the
		  computation itself. Also, the approach can be applied even
		  to highly optimizing compilers, as demonstrated by the fact
		  that our compiler generates target code, for a range of
		  realistic C programs, which is competitive with both the cc
		  and gcc compilers with all optimizations enabled. The
		  certifier also drastically improves the effectiveness of
		  compiler testing because, for each test case, it statically
		  signals compilation errors that might otherwise require
		  many executions to detect. Finally, this approach is a
		  practical way to produce the safety proofs for a
		  Proof-Carrying Code system, and thus may be useful in a
		  system for safe mobile code.},
  booktitle	= {Proceedings of the 1998 {ACM} {SIGPLAN} Conference on
		  Programming Language Design and Implementation (PLDI)}
}

@Article{	  Nelson/Oppen80,
  author	= {G. Nelson and D. Oppen},
  journal	= {JACM},
  number	= {2},
  pages		= {356-364},
  title		= {Fast decision procedures based on congruence closure},
  volume	= {27},
  year		= {1980}
}

@Article{	  Nielson82,
  author	= {Nielson, {F. A.}},
  title		= {A denotational framework for data flow analysis},
  journal	= {Acta Informatica},
  volume	= {18},
  pages		= {265--287},
  year		= {1982}
}

@Manual{	  Nuprl93,
  author	= {The Nuprl Group},
  edition	= {4.1},
  month		= mar,
  note		= {(Draft)},
  organization	= {Cornell University},
  title		= {The {Nuprl} Proof Development System},
  year		= {1993}
}

@Book{		  ODonnell85,
  author	= {{M.J.} {O'D}onnell},
  title		= {Equational Logic as a Programming Language},
  publisher	= {MIT Press},
  year		= {1985}
}

@inproceedings{Oheimb-Pusch-JavaDays98,
        author = {David von Oheimb and Cornelia Pusch},
        title = {Java -- formal fundiert},
        booktitle = {JIT'98 --- Java-Informations-Tage 1998},
        year = {1998},
        publisher = {Springer},
        series = {Informatik Aktuell},
        editor = {C. H. Cap},
        url = {http://www.in.tum.de/~isabelle/bali/papers/JavaDays98.html},
        abstract = {Dieser Artikel gibt eine Übersicht über das Projekt Bali zur formalen 
Behandlung möglichst vieler Aspekte von Java. Die Arbeiten umfassen bisher
eine formale Semantik großer Teile der Java-Quellsprache und des Bytecodes, 
jeweils zusammen mit einem Beweis der Typsicherheit. 
Als Spezifikations- und Verifikationswerkzeug dient Isabelle/HOL.
Wir beschreiben die Ziele dieses Projekts und die grobe Vorgehensweise, 
geben einen knappen Einblick in die Formalisierung und die bewiesenen Aussagen,
und stellen unsere bisherigen Ergebnisse und Erfahrungen dar.},
        CRClassification = {D.3.1, F.3.2},
        CRGenTerms = {Languages, Security, Verification},
        pages={p. 77--86}
}

@TechReport{	  Oliva/Wand92,
  author	= {{Dino P.} Oliva and Mitchell Wand},
  title		= {{A} {V}erified {C}ompiler for {P}ure {PreScheme}},
  institution	= {Northeastern University College of Computer Science},
  type		= {Technical Report},
  number	= {NU-CCS-92-5},
  address	= {Northeastern University},
  month		= feb,
  year		= {1992}
}

@Article{	  Oppacher/Suen88,
  author	= {F. Oppacher and E. Suen},
  journal	= {Journal of Automated Reasoning},
  volume	= {4},
  pages		= {69-100},
  title		= {{HARP}: A Tableau-Based Theorem Prover},
  year		= {1988}
}

@TechReport{	  Orbaek:93,
  author	= {Peter {\O}rb{\ae}k},
  title		= {{Analysis and Optimization of Actions}},
  year		= {1993},
  month		= {September},
  type		= {{M.Sc. dissertation}},
  note		= {URL: {\tt ftp://ftp.daimi.aau.dk/pub/empl/poe/index.html}},
  institution	= {Computer Science Department, Aarhus University, Denmark},
  abstract	= {In the past, a few compiler generators have been based on
		  the Action Semantics framework, but they have all suffered
		  from the inability to generate compilers whose performance
		  is comparable to hand-written compilers. In this thesis we
		  give a type-checker and an analysis encompassing binding
		  time analysis, flow analysis and constant propagation for a
		  statically typed subset of Action Notation including higher
		  order abstractions. The type-checker is proved safe with
		  respect to the operational semantics of Action Notation.
		  The analyses are used to optimize code in a compiler
		  generator capable of generating compilers for the SPARC
		  processor from specifications written in Action Notation.
		  The quality of the the SPARC code produced by the generated
		  compilers is comparable to code produced by commercial C
		  compilers.}
}

@InProceedings{	  Owre+92,
  author	= {S. Owre and {J. M.} Rushby and N. Shankar},
  booktitle	= {Proceedings 11th International Conference on Automated
		  Deduction CADE},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Artificial Intelligence},
  volume	= {607},
  month		= oct,
  pages		= {748-752},
  title		= {{PVS}: {A} {P}rototype {V}erification {S}ystem},
  address	= {Saratoga, NY},
  editor	= {Deepak Kapur},
  year		= {1992}
}

@InProceedings{	  Owre+93,
  author	= {S. Owre and J. Rushby and N. Shankar and {F.W. von}
		  Henke},
  booktitle	= {Proceedings FME'93: Industrial-Strength Formal Methods},
  key		= {Owre 93},
  month		= apr,
  pages		= {482--500},
  series	= {LNCS},
  volume	= {670},
  title		= {Formal verification of fault-tolerant architectures: some
		  lessons learned},
  year		= {1993}
}

@InProceedings{	  Palsberg92b,
  author	= {J. Palsberg},
  title		= {An automatically generated and provably correct compiler
		  for a subset of ADA},
  booktitle	= {IEEE International Conference on Computer Languages},
  year		= {1992}
}

@PhDThesis{	  Palsberg92a,
  author	= {Jens Palsberg},
  title		= {Provably Correct Compiler Generation},
  year		= {1992},
  school	= {Department of Computer Science, University of Aarhus},
  note		= {xii+224 pages},
  annote	= {We have designed , implemented, and proved the correctness
		  of a compiler generator that accepts action semantic
		  descriptions of imperative programming languages. We have
		  used it to generate compilers for both a toy language and a
		  non-trivial subset of Ada. The generated compilers emit
		  absolute code for an abstract RISC machine language that is
		  assembled into code for the SPARC and the HP Precision
		  Architecture. The generated code is an order of magnitude
		  better than that produced by compilers generated by the
		  classical systems of Mosses, Paulson, and Wand. Our machine
		  language needs no runtime type-checking and is thus more
		  realistic than those considered in previous compiler
		  proofs. We use solely algebraic specifications; proofs are
		  given in the initial model. The use of action semantics
		  makes the processable language specification easy to read
		  and pleasant to work with. We view our compiler generator
		  as the first step towards user-friendly and automatic
		  generation of realistic and provably correct compilers.},
  keywords	= {action semantics}
}

@InProceedings{	  Parnas94,
  author	= {Parnas, {David Lorge}},
  title		= {{I}nspection of {S}afety {C}ritical {S}oftware {U}sing
		  {P}rogram-{F}unction {T}ables},
  editor	= {Duncan, K. and Krueger, K.},
  booktitle	= {Proceedings of the 13th World Computer Congress 1994,
		  Volume 3},
  year		= {1994},
  publisher	= {Elsevier Science B.V. (North-Holland)}
}

@Book{		  Partsch90,
  author	= {H. Partsch},
  publisher	= {Springer-Verlag},
  series	= {Texts and Monographs in Computer Science},
  title		= {Specification and Transformation of Programs},
  year		= {1990}
}

@PhDThesis{	  Paulson81,
  author	= {L. Paulson},
  title		= {A compiler generator for semantic grammars},
  school	= {Stanford University},
  year		= {1981}
}

@InProceedings{	  Persch+83,
  author	= {Guido Persch and H.-S. Jansohn and W. Kirchg\"assner and
		  Rudolf Landwehr and Manfred Dausmann and Sophia
		  Drossopoulou and Gerhard Goos},
  title		= {Ada Compiler Karlsruhe Overview},
  year		= {1983},
  booktitle	= {Ada-Europe / Adatex Joint Conference on Ada},
  publisher	= {Commission of the European Communities},
  pages		= {2/1 -- 4},
  address	= {Br\"ussel}
}

@PhDThesis{	  Pettersson95,
  author	= {M. Pettersson},
  title		= {Compiling Natural Semantics},
  school	= {Linkoeping University},
  year		= {1995}
}

@TechReport{	  Pfeifer94,
  author	= {H. Pfeifer},
  institution	= {Universit{\"a}t Ulm},
  number	= {94--02},
  title		= {Reflexion von {\sc QED} in {\sc QED}},
  type		= {Korso Study Note},
  year		= {1994}
}

@Article{	  PierantonioKutter97b,
  author	= {P. W. Kutter and A. Pierantonio},
  title		= {The Formal Specification of Oberon},
  journal	= {Journal of Universal Computer Science},
  volume	= {Volume 5},
  year		= {1997}
}

@Article{Pnueli98,
  author =       "A. Pnueli and O. Shtrichman and M. Siegel",
  title =        "Translation Validation for Synchronous Languages",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1443",
  pages =        "235--250",
  year =         "1998",
}

@Article{Pnueli:98:CVT,
  author = 	 {Amir Pnueli and O. Shtrichman and M. Siegel},
  title = 	 {The Code Validation Tool (CVT)},
  journal = 	 {Int. J. on Software Tools for Technology Transfer},
  year = 	 1998,
  volume =	 2,
  number =	 2,
  pages =	 {192-201},
  annote =	 {Untertitel: Automatic verification of a compilation process}
}

@InProceedings{Pnueli98a,
  author =       "A. Pnueli and M. Siegel and E. Singermann",
  title =        "Translation Validation",
  booktitle =    "Tools and Algorithms for the Construction and
                  Analysis of Systems",
  series =       "Lecture Notes in Computer Science",
  volume =       "1384",
  pages =        "151--166",
  year =         "1998",
  publisher =    springer                 
}
                  

@Article{	  Poe97,
  author	= {A. Poetzsch-Heffter},
  title		= {{Prototyping realistic programming languages based on
		  formal specifications}},
  journal	= {Acta Informatica},
  volume	= {34},
  number	= {10},
  pages		= {737--772},
  year		= {1997},
  keyword	= {semantics, programming environments}
}


@InProceedings{Poetzsch-Heffter-Mueller99,
  author =       "A. Poetzsch-Heffter and P. M{\"u}ller",
  title =        "A Programming Logic for Sequential {J}ava",
  booktitle =    "European Symosium un Programming ({ESOP}~'99)",
  editor =       "S. D. Swierstra",
  series =       "Lecture Notes in Computer Science",
  year =         "1999",
  publisher =    "Springer-Verlag",
  note =         "(To appear)",
  url =          "http://www.informatik.fernuni-hagen.de/import/pi5/forschung/veroeffentlichungen/esop99.ps.gz",
}


@InProceedings{Poetzsch-HeffterMueller98,
  author =       "Arnd Poetzsch-Heffter and Peter M{\"u}ller",
  title =        "Logical Foundations for Typed Object-Oriented
                 Languages",
  editor =       "David Gries and Willem-Paul De~Roever",
  booktitle =    "Proc.\ {IFIP} Working Conference on Programming
                 Concepts and Methods {PROCOMET}, Shelter Island, USA",
  year =         "1998",
  publisher =    "Chapman \& Hall",
}


@Misc{		  Pofahl95,
  author	= {E. Pofahl},
  title		= {{Methods Used for Inspecting Safety Relevant Software}},
  howpublished	= {{In W. J. Cullyer, W. A. Halang, B.J. Kr\"amer (eds.):
		  High Integrity Programmable Electronic Systems,
		  Dagstuhl-Sem.-Rep. 107, p 13}},
  year		= {1995}
}

@InCollection{	  Polak81,
  author	= {W. Polak},
  editor	= {G. Goos, J. Hartmanis},
  number	= {124},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  title		= {Compiler Specification and Verification},
  booktitle	= {LNCS},
  year		= {1981}
}

@Article{	  Proebsting:1995:BAG,
  author	= {Todd A. Proebsting},
  title		= {{BURS} Automata Generation},
  journal	= {ACM Transactions on Programming Languages and Systems},
  volume	= {17},
  number	= {3},
  pages		= {461--486},
  month		= may,
  year		= {1995}
}

@unpublished{Pusch-TACAS99,
  author =	 {Cornelia Pusch},
  title =	 {Proving the Soundness of a {J}ava Bytecode Verifier
                  Specification in {Isabelle/HOL}},
  year =	 {1999},
  note =	 {To appear},
  CRClassification ={D.3.1, F.3.2},
  CRGenTerms =	 {Languages, Security, Verification},
}

@inproceedings{Pusch_TPiH1996,
  author =	 {Cornelia Pusch},
  title =	 {Verification of Compiler Correctness for the WAM},
  booktitle =	 {Theorem Proving in Higher Order Logics (TPHOLs'96),
                  P. 347-362.},
  year =	 {1996},
  publisher =	 {Springer-Verlag},
  editor =	 {J. von Wright and J. Grundy and J. Harrison},
  url =
                  {http://www4.informatik.tu-muenchen.de/papers/Pusch_TPiH1996.html},
  abstract =	 {Relying on a derivation of the Warren Abstract
                  Machine (WAM) by stepwise refinement of Prolog
                  models by B\"orger and Rosenzweig we present a
                  formalization of an operational semantics for
                  Prolog. Then we develop four refinement steps
                  towards the Warren Abstract Machine (WAM). The
                  correctness and completeness proofs for each step
                  have been elaborated with the theorem prover
                  Isabelle using the logic HOL. },
  CRClassification ={},
  CRGenTerms =	 {}
}

@Article{	  Pym/Wallen90a,
  author	= {David Pym and Lincoln Wallen},
  journal	= {10th CADE},
  pages		= {236-250},
  title		= {Investigations into proof-search in a system of
		  first-order dependent function types},
  volume	= {LNCS 449},
  year		= {1990}
}

@Book{		  Randell+95,
  title		= {Proceedings of Predictably Dependable Computing Systems
		  PDCS'95},
  author	= {B. Randell and {J.-C.} Laprie and H. Kopetz and B.
		  Littlewood (Eds.)},
  publisher	= {Esprit Basic Research Series, Springer-Verlag},
  year		= {1995}
}

@InProceedings{	  Reddy88,
  author	= {Reddy, {U.S.}},
  title		= {Objects as {C}losures: {A}bstract {S}emantics of {O}bject
		  {O}riented {L}anguages},
  booktitle	= {Proceedings of the 1988 ACM Conference on LISP and
		  Functional Programming},
  pages		= {289--297},
  year		= {1988}
}

@Misc{		  Robinson96,
  author	= {A. Robinson},
  title		= {Formal and Informal Proof},
  howpublished	= {{Vortrag im Kolloquium des DFG-Schwerpunktprogramms
		  ``Deduktion'', Dagstuhl}},
  year		= {1996},
  month		= jan
}

@PhDThesis{	  Rubinfeld90,
  author	= {R. Rubinfeld},
  title		= {A Mathematical Theory of Self-Checking, Self-Testing and
		  Self-Correcting Programs},
  institution	= {International Computer Science Institute},
  number	= {TR--90--054},
  howpublished	= {Technical Report},
  year		= {1990}
}

@article{ rubinfeld96designing,
    author = "Ronitt Rubinfeld",
    title = "Designing Checkers for Programs that Run in Parallel",
    journal = "Algorithmica",
    volume = "15",
    number = "4",
    pages = "287-301",
    year = "1996",
    url = "citeseer.nj.nec.com/rubinfeld94designing.html"
}

@TechReport{	  Ruess93,
  author	= {H. Rue{\ss}},
  institution	= {Universit{\"a}t Ulm},
  number	= {93--01},
  title		= {Report on the {S}pecification {L}anguage {\sc QED}},
  type		= {Korso Working Paper},
  year		= {1993}
}

@InProceedings{	  Ruess97:TLCA,
  author	= {Harald Rue{\ss}},
  title		= {{Computational Reflection in the Calculus of Constructions
		  and its Application to Theorem Proving}},
  year		= {1997},
  booktitle	= {Typed Lambda Calulus and Applications},
  note		= {Accepted for publication}
}

@Article{	  Rus98,
  author	= {T. Rus},
  title		= {Algebraic Processing of Programming Languages},
  journal	= {Theoretical Computer Science},
  year		= {1998},
  volume	= {199},
  pages		= {105--143}
}

@TechReport{	  Rushby+91,
  author	= {John Rushby and {Friedrich von Henke} and Sam Owre},
  address	= {Menlo Park, CA},
  institution	= {Computer Science Laboratory, SRI International},
  month		= feb,
  number	= {SRI--CSL--91--2},
  title		= {An Introduction to Formal Specification and Verification
		  Using {{\sc Ehdm}}},
  year		= {1991}
}

@Article{	  Rushby/vHenke93,
  key		= {Rushby 93},
  author	= {J. M. Rushby and {F.W. von} Henke},
  title		= {Formal verification of algorithms for critical systems},
  journal	= {IEEE Trans. on Software Engineering},
  year		= {1993},
  volume	= {19},
  number	= {1},
  month		= jan,
  pages		= {13--23}
}

@Unpublished{	  Rushby94,
  author	= {J. Rushby},
  month		= jan,
  note		= {Incomplete Draft},
  title		= {Proof Movie II: A Proof with PVS},
  year		= {1994}
}

@TechReport{	  Sampaio91,
  author	= {Augusto Sampaio},
  title		= {A Comparative Study of Theorem Provers: Proving
		  Correctness of Compiling Specifications},
  institution	= {Oxford University Computing Laboratory, Programming
		  Research Group},
  year		= {1991},
  key		= {PRG-TN-20-90}
}

@PhDThesis{	  Sampaio93,
  author	= {Augusto Sampaio},
  title		= {An Algebraic Approach to Compiler Design},
  school	= {Oxford University Computing Laboratory},
  year		= {1993},
  month		= oct,
  note		= {Technical Monograph PRG--110, Oxford University Computing
		  Laboratory},
  address	= {Programming Research Group}
}

@PhdThesis{Schellhorn99,
  author =    {Gerhard Schellhorn},
  title =    "{Verifikation abstrakter Zustandsmaschinen}",
  school =   "{Unversit\"at Ulm}",
  year =     "1999"
}

@Book{		  Schmidt,
  author	= {D. A. Schmidt},
  title		= {Denotational Semantics},
  publisher	= {Wm. C. Brown Publishers},
  year		= {1988},
  address	= {Dubuque, Iowa}
}

@Article{	  Schmidt85,
  author	= {D. A. Schmidt},
  title		= {Detecting global variables in denotational
		  specifications},
  journal	= {ACM Transactions on Programming Languages and Systems},
  volume	= {7},
  number	= {2},
  pages		= {299--310},
  year		= {1985}
}

@Article{	  Schmidt88,
  author	= {D. A. Schmidt},
  title		= {Detecting stack-based environments in denotational
		  definitions},
  journal	= {Science of Computer Programming},
  volume	= {11},
  pages		= {107--131},
  year		= {1988}
}

@TechReport{	  Schroeer88,
  author	= {{F. W.} Schr\"oer},
  title		= {Districts: A Foundation for the Suppression of Partial
		  Redundancies},
  institution	= {GMD-Berichte},
  number	= {304},
  year		= {1988}
}

@Article{	  Schroeer88b,
  author	= {{F. W.} Schr\"oer},
  title		= {Das GMD Modula-2 Entwicklungssystem},
  journal	= {GMD-Spiegel},
  volume	= {1},
  year		= {1988}
}

@PhDThesis{	  Schuerr91,
  author	= {Sch\"urr, Andreas},
  title		= {Operationales Spezifizieren mit programmierten
		  Graphersetzungssystemen},
  school	= {{Universit\"at Aachen, Deutscher Universit\"ats-Verlag}},
  year		= {1991}
}

@InProceedings{	  Schwarz+88,
  author	= {Schwarz, B. and Kirchg\"assner, W. and Landwehr, R.},
  title		= {An Optimizer for Ada - Design, Experiences and Results},
  booktitle	= {Proceedings of the ACM SIGPLAN '89 Conference on
		  Programming Language Design and Implementation},
  year		= {1989},
  month		= jun
}

@TechReport{	  Schwier93a,
  author	= {D. Schwier},
  institution	= {Universit{\"a}t Ulm},
  number	= {93--04},
  title		= {Semantik von {\sc QED}},
  type		= {Korso Working Paper},
  year		= {1993}
}

@TechReport{	  Schwier93b,
  author	= {D. Schwier},
  institution	= {Universit{\"a}t Ulm},
  number	= {93--05},
  title		= {Formale {P}rogrammentwicklung in {\sc QED}},
  type		= {Korso Study Note},
  year		= {1993}
}

@InProceedings{	  Shankar91,
  author	= {N. Shankar},
  booktitle	= {CADE-11},
  series	= {LNCS},
  volume	= {607},
  publisher	= {Springer-Verlag},
  title		= {Proof Search in the Intuitionistic Sequent Calculus},
  year		= {1991}
}

@Article{	  Shostak79a,
  author	= {Robert E. Shostak},
  journal	= {JACM},
  month		= apr,
  number	= {2},
  pages		= {361-360},
  title		= {A Practical Decision Procedure for Arithmetic with
		  Function Symbols},
  volume	= {26},
  year		= {1979},
  category	= {DecisionProcedures}
}

@TechReport{	  Simpson90,
  author	= {T. Simpson},
  address	= {Department of Computer Science, University of Calgary,
		  2500 University Drive N.W., Calgary, Alberta, Canada, T2N
		  1N4},
  institution	= {Department of Computer Science, University of Calgary,},
  month		= oct,
  number	= {90/410/34},
  title		= {Correctness of a Compiler Specification for the SECD
		  Machine},
  type		= {Research Report},
  year		= {1990}
}

@TechReport{	  Sites92,
  author	= {R. L. Sites},
  title		= {{Alpha architecture Reference Manual}},
  institution	= {Digital Equipment Corporation},
  year		= {1992}
}

@Book{		  Sites:Alpha92,
  author	= {Richard L. Sites},
  title		= {{Alpha} {A}rchitecture {R}eference {M}anual},
  publisher	= {Digital Equipment Corporation},
  year		= {1992}
}

@TechReport{	  Smith82,
  author	= {Smith, {B.C.}},
  title		= {{R}eflection and {S}emantics in a {P}rocedural
		  {L}anguage},
  institution	= {Massachusetts Institute of Technology},
  type		= {{T}echnischer {B}ericht},
  number	= {MIT-LCS-TR-272},
  address	= {Cambridge, MA},
  year		= {1982}
}

@InProceedings{	  Smith84,
  author	= {Smith, {B.C.}},
  title		= {{R}eflection and {S}emantics in {L}isp},
  booktitle	= {Proceedings of the 11th ACM Symposium on Principles of
		  Programming Languages POPL'84},
  pages		= {23-35},
  year		= {1984}
}

@TechReport{	  Smith87,
  author	= {D.R. Smith},
  address	= {Palo Alto, CA},
  institution	= {Kestrel Institute},
  number	= {KES.U.87.12},
  title		= {Structure and Desing of Global Search Algorithms},
  year		= {1987}
}

@inproceedings{SrivasMiller95:chdl,
        TITLE = {Applying Formal Verification to a Commercial Microprocessor},
        AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
        PAGES = {493--502},
        BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
                Description Languages and their Applications},
        EDITOR = {Steven D. Johnson},
        ORGANIZATION = {Proceedings published in a single volume jointly
                with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
                no.\ 95TH8102},
        MONTH = aug,
        YEAR = 1995,
        ADDRESS = {Chiba, Japan}
}

@MastersThesis{	  Ste98,
  author	= {Michael Stegm{\"u}ller},
  title		= {{Formale Verifikation des DLX RISC-Prozessors: Eine
		  Fallstudie basierend auf abstrakten Zustandsmaschinen}},
  school	= {Universit{\"a}t Ulm},
  year		= {1998}
}

@Book{		  Steele84,
  author	= {Steele, {G.L.}},
  title		= {{Common Lisp}: {T}he {L}anguage},
  publisher	= {Digital Press},
  address	= {Bedford, MA},
  year		= {1984}
}

@Book{		  Steele90,
  author	= {Steele, {G.L.}},
  title		= {{Common Lisp}: {T}he {L}anguage. Second Edition},
  publisher	= {Digital Press},
  address	= {Bedford, MA},
  year		= {1990}
}

@InProceedings{	  Steffen+89,
  author	= {Steffen, B. and Knoop, J. and R\"uthing, O.},
  title		= {{T}he {V}alue {F}low {G}raph: {A} {P}rogram
		  {R}epresentation {f}or {O}ptimal {P}rogram
		  {T}ransformations},
  booktitle	= {\mbox{$3^{rd}$} ESOP},
  series	= {LNCS},
  volume	= {432},
  pages		= {389--405},
  address	= {Copenhagen, Denmark},
  note		= {--\ Extended version available as: Bericht Nr. 9004,
		  Institut f\"ur Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit\"at Kiel, Germany, 1990},
  year		= {1990}
}

@InProceedings{	  Steffen+90,
  author	= {Steffen, B. and Knoop, J. and R\"uthing, O.},
  address	= {Copenhagen, Denmark},
  booktitle	= {Proc. 3$^{rd}$~European Symposium on Programming (ESOP)},
  pages		= {389 - 405},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  volume	= {432},
  title		= {The Value Flow Graph: {A} Program Representation for
		  Optimal Program Transformations},
  year		= {1990}
}

@InProceedings{	  Steffen+91,
  author	= {Steffen, B. and Knoop, J. and R\"uthing, O.},
  address	= {Brighton, UK},
  booktitle	= {Proc. 4$^{th}$~International Joint Conference on the
		  Theory and Practice of Software Development (TAPSOFT)},
  pages		= {394 - 415},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  volume	= {494},
  title		= {Efficient Code Motion and an Adaption to Strength
		  Reduction},
  year		= {1991}
}

@InProceedings{	  Steffen/Knoop89,
  author	= {Steffen, B. and Knoop, J.},
  address	= {Por\c{a}bka-Kozubnik, Poland},
  booktitle	= {Proc. 14$^{th}$ MFCS},
  pages		= {481-491},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  volume	= {379},
  title		= {Finite Constants: {C}haracterizations of a New Decidable
		  Set of Constants},
  year		= {1989}
}

@Article{	  Steffen/Knoop91,
  author	= {Steffen, B. and Knoop, J.},
  journal	= tcs,
  note		= {Extended version of \cite{Steffen/Knoop89}},
  number	= {2},
  pages		= {481-491},
  publisher	= {Springer-Verlag},
  title		= {Finite Constants: {C}haracterizations of a New Decidable
		  Set of Constants},
  volume	= {80},
  year		= {1991}
}

@InProceedings{	  Steffen87a,
  author	= {Steffen, B.},
  title		= {{O}ptimal {R}un {T}ime {O}ptimization. {P}roved {b}y {a}
		  {N}ew {L}ook {a}t {A}bstract {I}nterpretations},
  booktitle	= {\mbox{$2^{nd}$} TAPSOFT},
  series	= {LNCS},
  volume	= {249},
  publisher	= {Springer-Verlag},
  pages		= {52--68},
  address	= {Pisa, Italy},
  year		= {1987}
}

@PhDThesis{	  Steffen87b,
  author	= {Steffen, B.},
  title		= {{A}bstrakte {I}nterpretationen {b}eim {O}ptimieren {v}on
		  {P}rogrammlaufzeiten. {E}in {O}ptimalit\"atskonzept {u}nd
		  {s}eine {A}nwendung},
  school	= {Bericht Nr. 8713, Institut f\"ur Informatik und Praktische
		  Mathematik der Christian-Albrechts-Universit\"at},
  address	= {Kiel},
  year		= {1987}
}

@InProceedings{	  Steffen89,
  author	= {Steffen, B.},
  title		= {{O}ptimal {D}ata {F}low {A}nalysis {v}ia {O}bservational
		  {E}quivalence},
  booktitle	= {\mbox{$14^{th}$} MFCS},
  publisher	= {LNCS 397},
  pages		= {492--502},
  address	= {Por\c{a}bka-Kozubnik, Poland},
  year		= {1989}
}

@Book{		  Stoy77,
  author	= {Stoy, {J.E.}},
  title		= {{D}enotational {S}emantics: {T}he {S}cott--{S}trachey
		  {A}pproach to {P}rogramming {L}anguage {T}heory},
  publisher	= {MIT Press},
  address	= {Cambridge, MA., London},
  year		= {1977}
}

@TechReport{	  Symbolics85,
  author	= {{Symbolics Inc.}},
  title		= {Reference guide to {Symbolics} {LISP}},
  institution	= {Symbolics Inc.},
  address	= {Cambridge, MA},
  year		= {1985}
}

@TechReport{	  Symbolics86,
  author	= {{Symbolics Inc.}},
  title		= {Symbolics {Common Lisp}: {L}anguage {C}oncepts},
  institution	= {Symbolics Inc.},
  address	= {Cambridge, MA},
  year		= {1986}
}

@TechReport{	  Taiichi/Masami86,
  author	= {Taiichi, Y. and Masami, H.},
  title		= {{K}yoto {C}ommon {L}isp {R}eport},
  institution	= {Research Institute for Mathematical Science},
  address	= {Kyoto University},
  year		= {1986}
}

@TechReport{	  Tarditi+90,
  author	= {Tarditi, D. and Acharya, A. and Lee, P.},
  title		= {{N}o {A}ssembly required: {C}ompiling {S}tandard {ML} to
		  {C}.},
  institution	= {School of Computer Science, CMU},
  year		= {1990},
  number	= {CMU-CS-90-187},
  month		= dec
}

@Article{	  Thatcher+81,
  author	= {Thatcher, J. W. and Wagner, E. G. and Wright, J.B.},
  title		= {More on Advice on Structuring Compilers and Proving them
		  Correct},
  journal	= {Theoretical Computer Science},
  volume	= {15},
  year		= {1981},
  pages		= {223--249}
}

@Article{	  Thompson84,
  author	= {Ken Thompson},
  title		= {{Reflections on Trusting Trust}},
  journal	= {Communications of the ACM},
  volume	= {27},
  number	= {8},
  year		= {1984},
  pages		= {761--763},
  note		= {ACM Turing Award Lectures: The First Twenty Years
		  1965-1985, ACM Press, 1987, and in Computers Under Attack:
		  Intruders, Worms, and Viruses Copyright, ACM Press 1990}
}

@Book{		  Tofte90,
  author	= {M. Tofte},
  title		= {Compiler Generators},
  publisher	= {Springer-Verlag},
  year		= {1990}
}

@Book{		  Uhl86,
  author	= {J. Uhl},
  title		= {Spezifikation von Programmiersprachen und \"Ubersetzern},
  series	= {GMD-Berichte},
  volume	= {161},
  publisher	= {Oldenburg-Verlag},
  year		= {1986}
}

@InProceedings{	  Vollmer/Hoffart92,
  author	= {J. Vollmer and R. Hoffart},
  title		= {Modula-P, a Language For Parallel Programming; Definition
		  and Implementation on a Transputer Network},
  booktitle	= {IEEE International Conference on Computer Languages},
  year		= {1992}
}

@Book{		  WaiteGoos:84:Compiler,
  author	= {William M. Waite and Gerhard Goos},
  title		= {{C}ompiler {C}onstruction},
  year		= {1984},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  WallaceC++95,
  author	= {C. Wallace},
  title		= {{T}he {S}emantics of the {C++}--{P}rogramming {L}anguage},
  editor	= {E. B\"orger},
  booktitle	= {Specification and Validation Methods},
  publisher	= {Oxford University Press},
  year		= {1995}
}

@Book{		  Wallen90,
  author	= {{Lincoln A.} Wallen},
  publisher	= {MIT Press},
  title		= {Automated proof search in non-classical logics},
  year		= {1990}
}

@InProceedings{	  Wand/Friedman86,
  author	= {Wand, M. and Friedman, {D.P.}},
  title		= {{T}he {M}ystery of the {T}ower {R}evealed: {A}
		  {N}on-{R}eflective {D}escription of the {R}eflective
		  {T}ower},
  booktitle	= {Proceedings of the 1986 ACM-Conference on Lisp and
		  Functional Programming},
  pages		= {298-307},
  address	= {Cambridge, MA},
  year		= {1986}
}

@Article{	  Wand84,
  author	= {Wand, M.},
  title		= {A semantic prototyping system},
  journal	= {SIGPLAN Notices},
  note		= {SIGPLAN 84 Symp. On Compiler Construction},
  volume	= {19},
  number	= {6},
  pages		= {213--221},
  month		= jun,
  year		= {1984}
}

@InProceedings{	  Wand87,
  author	= {Wand, M.},
  title		= {Complete {T}ype {I}nference for {S}imple {O}bjects},
  booktitle	= {Proceedings of the {IEEE} Symposium on Logic in Computer
		  Science},
  pages		= {37--44},
  address	= {Ithaca, N.Y.},
  year		= {1985}
}

@Article{	  Weber-Wulff93,
  author	= {Weber-Wulff, Deborah},
  journal	= {Formal Aspects of Computing},
  number	= {2},
  pages		= {121--151},
  title		= {Proof Movie -- a proof with the Boyer-Moore prover},
  volume	= {5},
  year		= {1993}
}

@Book{		  Weber91,
  author	= {M. Weber},
  title		= {A Meta Calculus for Formal System Development},
  series	= {GMD--Berichte},
  publisher	= {Oldenbourg-Verlag},
  volume	= {195},
  year		= {1991}
}

@InProceedings{	  Weule93,
  author	= {Weule, H.},
  editor	= {Puppe, F. and G\"unter, A.},
  title		= {{E}xpertensysteme im industriellen {E}insatz},
  booktitle	= {Expertensysteme '93},
  publisher	= {Informatik aktuell, Springer-Verlag},
  address	= {Berlin, Heidelberg, New York},
  year		= {1993}
}

@Book{		  Wirth77,
  author	= {N. Wirth},
  title		= {{Compilerbau}},
  publisher	= {Teubner},
  year		= {1977}
}

@InProceedings{	  Woodcock/Morgan90,
  author	= {Woodcock, {J.C.P.} and Morgan, Carroll},
  editor	= {D. Bj\o rner and {C.A.R.} Hoare and H. Langmaack},
  title		= {{R}efinement of {S}tate {B}ased {C}oncurrent {S}ystems},
  booktitle	= {Proc. of the 3. International Symposium of VDM Europe
		  VDM'90},
  series	= {LNCS},
  volume	= {428},
  publisher	= {Springer-Verlag},
  address	= {Kiel},
  year		= {1990}
}

@Book{		  Wynskel,
  author	= {G. Wynskel},
  title		= {The Formal Semantics of Programming Languages},
  publisher	= {MIT Press},
  year		= {1993},
  series	= {Foundations of Computing Series},
  address	= {Cambridge, Massachusetts}
}

% Dold95:AMAST = Dold95
@TechReport{	  Young88,
  author	= {W.D. Young},
  address	= {Austin, Texas},
  institution	= {Comp. Logic. Inc.},
  number	= {33},
  title		= {A Verified Code Generator for a Subset of Gypsy},
  year		= {1988}
}

@Misc{		  ZSI89,
  author	= {{ZSI-Zentralstelle f\"ur Sicherheit in der
		  In\-for\-ma\-tions\-technik}},
  title		= {{IT-Sicherheitskriterien}},
  howpublished	= {Bundesanzeiger Verlagsgesellschaft, K\"oln},
  year		= {1989}
}

@Misc{		  ZSI90,
  author	= {{ZSI-Zentralstelle f\"ur Sicherheit in der
		  In\-for\-ma\-tions\-technik}},
  title		= {{IT-Evaluationshandbuch}},
  howpublished	= {{Bundesanzeiger Verlagsgesellschaft, K\"oln}},
  year		= {1990}
}

@Book{		  Zimmermann90,
  author	= {W. Zimmermann},
  title		= {Automatische Komplexit{\"a}tsanalyse funktionaler
		  Programme},
  series	= {Informatik-Fachberichte},
  volume	= {261},
  publisher	= {Springer-Verlag},
  year		= {1990}
}


@InProceedings{	  diPrimio+85,
  author	= {diPrimio, F. and Bungers, D. and Christaller, Th.},
  title		= {{BABYLON} als {W}erkzeug zum {A}ufbau von
		  {E}xpertensystemen},
  booktitle	= {Informatik--Fachberichte Nr. 112 ``Wissensbasierte
		  Systeme''},
  editor	= {Brauer, W. and Radig, B.},
  publisher	= {Springer-Verlag},
  pages		= {234--245},
  address	= {Berlin},
  year		= {1985}
}


@InProceedings{	  nymeyer.96a,
  author	= {Nymeyer, Albert and Katoen, Joost-Pieter and Westra, Ymte
		  and Alblas, Henk},
  title		= {{Code Generation = A* + BURS}},
  booktitle	= {Compiler Construction (CC)},
  year		= {1996},
  editor	= {Gyimothy, Tibor},
  pages		= {160--176},
  publisher	= {Springer-Verlag},
  address	= {{H}eidelberg},
  volume	= {1060},
  series	= {LNCS},
  month		= apr,
  note		= {}
}

@InProceedings{popl85*334,
  author =       "Alfred V. Aho and Mahadevan Ganapathi",
  title =        "Efficient Tree Pattern Matching: an Aid to Code
                 Generation",
  pages =        "334",
  ISBN =         "0-89791-147-4",
  editor =       "Brian K. Reid",
  booktitle =    "Conference Record of the 12th Annual {ACM} Symposium
                 on Principles of Programming Languages",
  address =      "New Orleans, LS",
  month =        jan,
  year =         "1985",
  publisher =    "ACM Press",
}

@TechReport{	  nymeyer.96b,
  author	= {Nymeyer, Albert and Katoen, Joost-Pieter},
  title		= {{Code Generation based on formal BURS theory and heuristic
		  search}},
  institution	= {University of Twente},
  type		= {Technical Report INF 95-42},
  year		= {1996},
  annote	= {rd=30/4/96. loc=ua. Extended article. very good overview
		  on BUPM and BURS. A* search for resolving indeterminism.}
}

@InCollection{	  procos2:BHP94,
  author	= {J. P. Bowen and {He Jifeng} and I. Page},
  title		= {Hardware Compilation},
  editor	= {J. P. Bowen},
  booktitle	= {Towards Verified Systems},
  publisher	= {Elsevier},
  series	= {Real-Time Safety Critical Systems},
  volume	= {2},
  year		= {1994},
  chapter	= {10},
  pages		= {193--207}
}

@Article{ JifengBowen94, 
  title         = "Specification, Verification and Prototyping of an Optimized Compiler",
  author        = "He Jifeng and Jonathan Bowen",
  journal       = "Formal Aspects of Computing",
  volume        = "6",
  number        = "6",
  pages         = "643--658",
  year          = "1994",
} 

@InProceedings{	  vHenke+94,
  author	= {{F.W. von} Henke and A. Dold and M. Grosse and H. Rue{\ss}
		  and D. Schwier and M. Strecker},
  booktitle	= {Arbeitsberichte des {\sc Korso}-Projekts},
  note		= {Erscheint im Laufe des Jahres},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  title		= {Construction and {D}eduction {M}ethods for the {F}ormal
		  {D}evelopment of {S}oftware},
  year		= {1994}
}


@Book{Wirth86,
  author =       "N. Wirth",
  title =        "Compilerbau",
  publisher =    "Springer",
  address =      "Berlin",
  year =         "1986",
  descriptor =   "Robotik",
}

@Article{	  Goos:97:Sather-K,
  author	= {Gerhard Goos},
  title		= "{Sather-K --- The Language}",
  journal	= {Software --- Concepts and Tools},
  volume	= 18,
  pages		= {91-109},
  year		= 1997,
  url		= "ftp://i44ftp.info.uni-karlsruhe.de/pub/papers/ggoos/satherk.ps.gz"
		  
}

@Book{Bhandarkar:1996:AIA,
  author =       "Dileep P. Bhandarkar",
  title =        "{Alpha} implementations and architecture: complete
                 reference and guide",
  publisher =    "Digital Press",
  address =      "12 Crosby Drive, Bedford, MA 01730, USA",
  pages =        "xviii + 328",
  year =         "1996",
  ISBN =         "1-55558-130-7",
  LCCN =         "QA76.8.A176B47 1996",
  bibdate =      "Thu Aug 07 13:42:54 1997",
  price =        "US\$41.95",
  acknowledgement = ack-nhfb,
}

@Misc{Sterkenburg2000a,
  author =	 {Reinier Sterkenburg},
  title =	 {Borland Pascal Compiler Bug List},
  howpublished = {http://www.dataweb.nl/~r.p.sterkenburg/bugsall.htm},
  year =	 {2000},
  month =	 {feb}
}

@Misc{Sun2000a,
  author =	 {Sun Microsystems},
  title =	 {Sun official Java Compiler Bug Database},
  howpublished = {http://java.sun.com/products/jdk/1.2/bugs.html},
  year =	 {2000},
  month =	 {mar}
}

@Misc{Inprise2000a,
  author =	 {Borland/Inprise},
  title =	 {Official Borland/Inprise Delphi-5 Compiler Bug List},
  howpublished = {http://www.borland.com/devsupport/delphi/fixes/delphi5/compiler.html},
  year =	 {2000},
  month =	 {jan},
  note =	 {Delphi5 Compiler Bug List}
}

@Misc{Inprise1999b,
  author =	 {Borland/Inprise},
  title =	 {Official Borland/Inprise Delphi-4 Compiler Bug List},
  howpublished = {http://www.borland.com/devsupport/delphi/fixes/delphi5/compiler.html},
  year =	 {1999},
  month =	 {jul},
  note =	 {Delphi4 Compiler Bug List}
}

@Misc{Inprise1999a,
  author =	 {Borland/Inprise},
  title =	 {Official Borland/Inprise Delphi-3 Compiler Bug List},
  howpublished = {http://www.borland.com/devsupport/delphi/fixes/3update/compiler.html},
  year =	 {1999},
  month =	 {jul},
  note =	 {Delphi3 Compiler Bug List}
}

@InProceedings{BlumK89,
title={Designing Programs That Check Their Work},
author={Blum, Manuel and Kannan, Sampath},
pages={86--97},
crossref={STOC21},
source={http://theory.lcs.mit.edu/~dmjones/STOC/stoc.bib}
}

@Proceedings{STOC21,
title={Proceedings of the Twenty First Annual ACM Symposium on Theory
of Computing},
booktitle={Proceedings of the Twenty First Annual ACM Symposium on
Theory of Computing},
pages = {15--17 },
month= {may},
year=1989,
address={Seattle, Washington},
c-organization={ACM},
key={ACM},
crossrefonly=1,
source={http://theory.lcs.mit.edu/~dmjones/STOC/stoc.bib}
}

@InProceedings{BlumW94,
title={Program Result-Checking: A Theory of Testing Meets a Test of
Theory},
author={Manuel Blum and Hal Wasserman},
pages={382--392},
crossref={FOCS35},
source={http://theory.lcs.mit.edu/~dmjones/FOCS/focs.bib}
}

@Proceedings{FOCS35,
title={35th Annual Symposium on Foundations of Computer Science},
booktitle={35th Annual Symposium on Foundations of Computer
Science},
month= nov,
pages = {20--22 },
year=1994,
address={Santa Fe, New Mexico},
organization={IEEE},
crossrefonly=1,
source={http://theory.lcs.mit.edu/~dmjones/FOCS/focs.bib}
}

@Inproceedings{ CGTV99,
  author        = "Alessandro Cimatti and Fausto Giunchiglia and Paolo
                  Traverso and Adolfo Villafiorita",
  title         = {{Run-Time Result Verification of Safety Critical
                  Software: and Industrial Case Study}}, 
  year          = 1999,
  booktitle     = "Proceedings of {RTRV} '99: Workshop on Runtime
                  Result Verification",
  editor        = {Amir Pnueli and Paolo Traverso},
  Address       = {Trento, Italy},
  file          = {RTRV99}
}

@Inproceedings{ RM99,
  author        = "Martin C. Rinard and Darko Marinov",
  title         = {{Credible Compilation with Pointers}}, 
  year          = 1999,
  booktitle     = "Proceedings of {RTRV} '99: Workshop on Runtime
                  Result Verification",
  editor        = {Amir Pnueli and Paolo Traverso},
  Address       = {Trento, Italy},
  file          = {RTRV99}
}

@misc{gcc2001,
  author        = {Free Software Foundation},
  title         = {The GNU GCC project},
  year          = 2001,
  howpublished  = {http://www.gnu.org/software/gcc/gcc.html},
}
@misc{gccbug2001,
  author        = {Free Software Foundation},
  title         = {The GNU GCC project bug database},
  year          = 2001,
  howpublished  = {http://gcc.gnu.org/cgi-bin/gnatsweb.pl},
}

%% neu 28.2.02:

%%% doppelt:(!)
@inproceedings{ necula98design,
    author = "George C. Necula and Peter Lee",
    title = "The Design and Implementation of a Certifying Compiler",
    booktitle = "Proceedings of the {ACM} {SIGPLAN}'98 Conference on Programming Language Design and Implementation ({PLDI})",
    month = "17--19~",
    address = "Montreal, Canada",
    pages = "333--344",
    year = "1998",
    url = "citeseer.nj.nec.com/necula98design.html" 
}

@inproceedings{ necula97proofcarrying,
    author = "George C. Necula",
    title = "Proof-Carrying Code",
    booktitle = "Conference Record of {POPL}~'97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
    month = "15--17",
    address = "Paris, France",
    pages = "106--119",
    year = "1997",
    url = "citeseer.nj.nec.com/49901.html"
}

@inproceedings{ necula01oraclebased,
    author = "George C. Necula and S. P. Rahul",
    title = "Oracle-based checking of untrusted software",
    booktitle = "Symposium on Principles of Programming Languages",
    pages = "142-154",
    year = "2001",
    url = "citeseer.nj.nec.com/necula01oraclebased.html"
}

@inproceedings{ colby00certifying,
    author = "Christopher Colby and Peter Lee and George C. Necula and Fred Blau and Mark Plesko and Kenneth Cline",
    title = "A certifying compiler for Java",
    booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
    pages = "95-107",
    year = "2000",
    url = "citeseer.nj.nec.com/colby00certifying.html"
}

@inproceedings{ necula01scalable,
    author = "George C. Necula",
    title = "A Scalable Architecture for Proof-Carrying Code",
    booktitle = "{FLOPS}",
    pages = "21-39",
    year = "2001",
    url = "citeseer.nj.nec.com/necula01scalable.html",
    kommentar = "eine weitere Arbeit zu Proof Carrying Code, hier
                  werden Optimierungen der Beweisstrategien gezeigt"
}

@inproceedings{ necula00translation,
    author = "George C. Necula",
    title = "Translation validation for an optimizing compiler",
    booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
    pages = "83-94",
    year = "2000",
    url = "citeseer.nj.nec.com/necula00translation.html",
    kommentar = "wichtige neue Arbeit von Necula zur
                  Validierung/Verifikation von
                  Optimierungen. Demonstriert am GCC/RTL wird die
                  automatische Validierung von Transformationen der RTL"
}

@misc{ necula02ccured,
  author = "G. Necula and S. McPeak and W. Weimer",
  title = "CCured: Type-safe retrofitting of legacy code",
  text = "George C. Necula, Scott McPeak, and Westley Weimer. CCured: Type-safe retrotting
    of legacy code. In Twenty-Ninth ACM Symposium on Principles of Programming
    Languages, Portland, OR, January 2002. To appear.",
  year = "2002",
  url = "citeseer.nj.nec.com/necula02ccured.html" 
}

@Article{KIV:99,
  author = 	 {W. Reif},
  title = 	 "{Formale Methoden für sicherheitskritische Software
                  -- Der KIV Ansatz}",
  journal = 	 {Informatik Forschung und Entwicklung},
  year = 	 {1999},
  volume =	 {14},
  number =	 {4},
  pages =	 {193-202},
  annote =	 {Argumentation für Verifikation (maschinell
                  unterstützt). Beispiele von Unglücken aufgrund von
                  Entwurfs-, Spezifikations- und
                  Implementierungsfehlern, Argumentation für
                  Modularisierung von Korrektheitsbeweisen,
                  automatischer Beweisführung und Wiederverwendung von
                  Beweisen. },
}

@Article{IEEETSE::ButlerF1993,
  author = "Ricky W. Butler, George B. Finelli",
  title = "The Infeasibility of Quantifying the Reliability of
                  Life-Critical Real-Time Software",
  journal = "IEEE Transactions on Software Engineering",
  year = 1993,
  volume = 19,
 number = 1,
 pages = {3--12},
abstract = {This paper affirms that the quantification of
                  life-critical software reliability is infeasible
                  using statistical methods whether applied to
                  standard software or fault-tolerant software. The
                  classical methods of estimating reliability are
                  shown to lead to exhorbitant amounts of testing when
                  applied to life-critical software. Reliability
                  growth models are examined and also shown to be
                  incapable of overcoming the need for excessive
                  amounts of testing. The key assumption of software
                  fault tolerance-separately programmed versions fail
                  independently-is shown to be problematic. This
                  assumption cannot be justified by experimentation in
                  the ultrareliability region and subjective arguments
                  in its favor are not sufficiently strong to justify
                  it as an axiom. Also, the implications of the recent
                  multiversion software experiments support this
                  affirmation.}
}

@article{ wahbe93efficient,
    author = "Robert Wahbe and Steven Lucco and Thomas E. Anderson and Susan L. Graham",
    title = "Efficient Software-Based Fault Isolation",
    journal = "ACM SIGOPS Operating Systems Review",
    volume = "27",
    number = "5",
    month = "December",
    pages = "203--216",
    year = "1993",
    url = "citeseer.nj.nec.com/wahbe93efficient.html" 
}