% Diese Datei enthaelt alle Bibs die keine echten Veroeffentlichungen
% sind aber trotzdem referenziert werden sollen oder wurden.
% Also insbesondere auch Verifix-Arbeitsberichte....

@Misc{Verifix-Antrag:94,
  Author        = {Gerhard Goos and Hans Langmaack and {F.W. von} 
                  Henke and Wolfgang Goerigk and Wolf Zimmermann},
  Title         = {{Verifizierte \"U}bersetzer ({{\em {Verifix}\/}})},
  Year          = {1994},
  Address       = {Karlsruhe, Kiel, Ulm},
  Howpublished  = {DFG-Projektantrag. Karlsruhe, Kiel, Ulm},
  verifixkey    = {ALL-VR},
  file          = {antrag}
}

@Misc{Verifix-Zwischenbericht:96,
  Author        = {Axel Dold and Thilo Gaul and Wolfgang Goerigk and Gerhard
                  Goos and Andreas Heberle and Friedrich von Henke and
                  Ulrich Hoffmann and Hans Langmaack and Holger
                  Pfeiffer  and Harald Ruess and Wolf Zimmermann},
  Title         = {Zwischenbericht {{\em {Verifix}\/}}},
  Year          = {1996},
  Address       = {Karlsruhe, Kiel, Ulm},
  Howpublished  = {DFG-Zwischenbericht. Karlsruhe, Kiel, Ulm},
  verifixkey    = {ALL-VR},
  file          = {Zwischenbericht}
}

@TechReport{	  Goerigk97-2.8,
  author	= {Goerigk, Wolfgang},
  title		= {Denotational Semantics for ComLisp and SIL},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  institution	= {CAU Kiel},
  number	= {Verifix/CAU/2.8},
  year		= {1997},
  note          = {(Draft)},
  verifixkey    = {CAU-VR},
  file          = {ComLispSIL}
}

@TechReport{	  Goerigk95b,
  author	= {Goerigk, Wolfgang},
  title		= {{Transputer State and Instruction Set Specification and
		  Initial Boot Protocol}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/2.1},
  year		= {1995},
  month		= jul,
  note          = {(Draft)},
  verifixkey    = {ULM-VR},
  file          = {transputer}
}

@TechReport{	  Goerigk96b,
  author	= {Goerigk, Wolfgang},
  title		= {{An Exercise in Program Verification: The ACL2 Correctness
		  Proof of a Simple Theorem Prover}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/2.4},
  year		= {1996},
  verifixkey    = {ULM-VR},
  file          = {Prover}
}

@TechReport{	  Goerigk/Hoffmann96,
  author	= {Goerigk, Wolfgang and Hoffmann, Ulrich},
  title		= {{T}he {C}ompiler {I}mplementation {L}anguage {ComLisp}},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  institution	= {CAU Kiel},
  number	= {Verifix/CAU/1.7},
  year		= {1996},
  month		= jun,
  file          = {comlisp-english}
}

@TechReport{      Goerigk/Hoffmann97-2.6,
  Author        = {Goerigk, Wolfgang and Hoffmann, Ulrich},
  Title         = {{Rigorous Compiler Implementation Correctness: How
		  to Prove the Real Thing Correct}},
  Year          = {1997},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  institution	= {CAU Kiel},
  number	= {Verifix/CAU/2.6},
  month		= jan,
  note          = {replaced by article in proceedings FM-TRENDS'98},
  file          = {realthing}
}

@TechReport{	  Goerigk/Mueller-Olm96,
  author	= {Goerigk, Wolfgang and M\"uller-Olm, Markus},
  title		= {{Erhaltung partieller Korrektheit bei beschr\"ankten
		  Maschinenressourcen. -- Eine Beweisskizze --}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/2.5},
  year		= {1996},
  file          = {Partial}
}

@TechReport{	  Hoffmann96d-3.1,
  author	= {Hoffmann, Ulrich},
  title		= {{\"Uber die korrekte Implementierung von Compilern}},
  institution	= {CAU Kiel},
  year		= {1996},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  note		= {replaced by article in proceedings of Work\-shop
                  {\sl ``Alternative Konzepte f\"ur Sprachen und
                  Rechner''}, Bad Honnef, 1996},
  number	= {Verifix/CAU/3.1},
  file          = {honnef96}
}


@TechReport{Hoffmann96a,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzung von {\sc intermediateC} in den
                  Assemblercode {\sc Tasm} des Transputers}},
  Institution   = {CAU Kiel},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Number        = {Verifix/CAU/1.6},
  Year          = {1996},
  Month         = jun,
  file          = {c2tasm-compiling-spec}
}

@TechReport{Hoffmann96b,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzung von {\sc ComLisp} in die 
                  Compiler--Zwischensprache Cop}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.8},
  Year          = {1996},
  Month         = jun,
  file          = {comlisp2cop-compiling-spec}
}

@TechReport{Hoffmann96c,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzung von Cop nach {\sc intermediateC}}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.9},
  Year          = {1996},
  Month         = jun,
  file          = {sil2cint-compiling-spec}
}

@TechReport{Hoffmann96f,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Das \"Ubersetzerprogramm von {\sc ComLisp} nach
                  Cop}},
  Institution   = {CAU Kiel},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Number        = {Verifix/CAU/1.10},
  Year          = {1996},
  Month         = jun,
  file          = {cl2cop-program}
}


@TechReport{	  Hoffmann96g,
  author	= {Hoffmann, Ulrich},
  title		= {{Das \"Ubersetzerprogramm von Cop nach {\sc
		  intermediateC}}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/1.11},
  year		= {1996},
  month		= jun,
  note          = {enthalten in CAU-Institutsbericht 9812}
}

@TechReport{	  Hoffmann96h,
  author	= {Hoffmann, Ulrich},
  title		= {{Korrekte Programmkonstruktion in {\sc ComLisp}}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/1.12},
  year		= {1996},
  month		= jun,
  note          = {enthalten in CAU-Institutsbericht 9812}
}

@TechReport{	  Hoffmann96i,
  author	= {Hoffmann, Ulrich},
  title		= {{Das \"Ubersetzerprogramm von {\sc intermediateC} nach
		  {\sc Tasm}}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/1.13},
  year		= {1996},
  month		= jun,
  note          = {enthalten in CAU-Institutsbericht 9812}
}

@TechReport{	  Hoffmann96j,
  author	= {Hoffmann, Ulrich},
  title		= {{Das \"Ubersetzerprogramm von {\sc Tasm} nach {\sc TC}}},
  institution	= {CAU Kiel},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/CAU/1.6},
  year		= {1996},
  month		= jun,
  note          = {enthalten in CAU-Institutsbericht 9812}
}

%%%%%%

@TechReport{Mueller-Olm96b,
  Author        = {Markus M\"uller-Olm},
  Title         = {{Three Views on Preservation of Partial Correctness}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/5.1},
  Year          = {1996},
  Month         = oct,
  file          = {part-cor}
}

@TechReport{Langmaack96b,
  Author        = {Langmaack, H.},
  Title         = {{Softwareengineering zur Zertifizierung von
                  Systemen: Spezifikations-, Implementierungs-,
                  \"Ubersetzerkorrektheit}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/4.1},
  Year          = {1996},
  Month         = aug,
  Note          = {Erscheint in Informationstechnik und Technische
                  Informatik it-ti, Oldenbourg Verlag},
  file          = {zertifiz}
}

@Inproceedings{Hoffmann97b,
  Author        = {U.\ Hoffmann},
  Title         = {{Correct Implementation of Compiler Programs}},
  BookTitle     = {Workshop on Programming Languages and Fundamentals of
                   Programming, Avendorf September 1997},
  editor =       {Rudolf Berghammer and Friedemann Simon},
  series =       {Technical Report 9717},
  year =         1997,
  publisher =    CAUIFIUPM,
  address =      {Kiel},
  month =        nov,
  pages =        {127--138},
  verifixkey    = {CAU-Pub},
  file          = {Hoffmann97-Avendorf}
}

%
% interne Verifix-Berichte Karlsruhe
%		  
		  		  
@TechReport{Verifix95:ISinformell,
  author = 	 {A. Dold and T. Gaul and W. Goerigk and G. Goos and
                  A. Heberle and F. von Henke and U. Hoffmann and
                  H. Langmaack and H. Pfeifer and H. Ruess and W. Zimmermann},
  title = 	 "{D}efinition of the {L}anguage {IS}",
  institution =  "University of Karlsruhe/Kiel/Ulm",
  type = 	 {Verifix Working Paper},
  number = 	 "[Verifix/UKA/1]",
  Year          = 1995,
  verifixkey    = {UKA-VR},
  file          = {ISinformell}
}
		  
@techreport{Verifix98:IS,
  author = {Andreas Heberle and Dirk Heuzeroth},
  title = {The Formal Specification of {IS}}, 
  institution = {IPD, {U}niversit\"at {K}arlsruhe},
  month = jan,
  number = "[Verifix/UKA/2 revised]",
  year = 1998,
  verifixkey    = {UKA-VR},
  file          = {ISsem}
}

@TechReport{Verifix96:MIS1,
  author =       {T.S. Gaul and A. Heberle and D. Heuzeroth and W. Zimmermann},
  title =        "An {ASM} {S}pecification of the
                  {O}perational {S}emantics of {MIS}",
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/3 revised]",
  Year          = 1996,
  verifixkey    = {UKA-VR},
  file          = {MIS-1-2}
}
		  
@TechReport{Verifix95:Alpha,
  author =       {T.S. Gaul},
  title =        "An {A}bstract {S}tate {M}achine {S}pecification of
                  the {DEC}-{A}lpha {P}rocessor {F}amily", 
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/4]",
  Year          = 1995,
  verifixkey    = {UKA-VR},
  file          = {Alpha_EvA}
}

@TechReport{Verifix96:MIS1toAlphaSimple,
  author = 	 {T.S. Gaul},
  title = 	 "Simple Code-generation for MIS to {DEC}-{A}lpha {P}rocessor
		  {F}amily", 
  institution =  "University of Karlsruhe",
  type = 	 {Verifix Working Paper},
  number = 	 "[Verifix/UKA/5]",
  Year          = 1996,
  verifixkey    = {UKA-VR},
  file          = {MIS1toAlphaSimple}
}

@TechReport{Verifix96:SemAnalyse0, 
  author =       {A. Heberle and W. Zimmermann and G. Goos},
  title =        "{S}pecification and {V}erification of {C}ompiler {F}rontend
                  {T}asks: {S}emantic {A}nalysis", 
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/7]",
  Year          = 1996,
  verifixkey    = {UKA-VR},
  file          = {SemanticAnalysis}
}
		  

@TechReport{Verifix96:Bench,
  author =       {T.S. Gaul},
  title =        "Bechmarking code-generation for {IS} to {DEC}-{A}lpha", 
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/11]",
  Year          = 1996,
  verifixkey    = {UKA-VR},
  file          = {BenchIS2Alpha}
}

@Techreport{ZG:97, 
  author =       {W. Zimmermann and T. Gaul},
  title =        "{An Abstract State Machine for Java Byte Code}",  
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/12]", 
  Year          = 1997,
  verifixkey    = {UKA-VR},
  file          = {JBCSem}
}

@TechReport{Verifix96:MIStoAlphaProof,
  author =       {T.S. Gaul and A. Lange},
  title =        "{V}erifiziertes {C}odeerzeugungsschema f{\"u}r die
		  {DEC}-{A}lpha {P}rozessor-{F}amilie",  
  institution =  "University of Karlsruhe",
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/13]",
  Year          = 1996,
  verifixkey    = {UKA-VR},
  file          = {MIS1toAlphaSimpleProofs2}
}

@TechReport{IntSpec:97,
  author = {Andreas Heberle and Dirk Heuzeroth},
  title = {Algebraische {S}pezifikation eines generischen
		  {I}nteger-{D}atentyps}, 
  institution = {IPD, {U}niversit\"at {K}arlsruhe},
  number =       "[Verifix/UKA/14]",
  verifixkey =   {UKA-VR},
  year = 1997,
  file          = {IntSpec1}
}

		  		  
@Unpublished{AGGZ:99,
  author =       "Andreas Heberle and Thilo Gaul and Wolfgang Goerigk
                  and Gerhard Goos and Wolf Zimmermann",
  title =        {{Construction of Verified Compiler Front-Ends
                  with Program-Checking}}, 
  year =         "1999",
  note =         "Working Paper, submitted to PSI99",
  verifixkey =   {UKA-VR},
  file          = {CheckedFrontend}
}

@TechReport{Zimmer-et-al:98,
  author        = {Wolfgang Goerigk and Wolf Zimmermann and Thilo Gaul and
		  Andreas Heberle and Ulrich Hoffmann},
  title         = {Correct Compilation of a While-Language with Parameterless
		  Recursive Procedures}, 
  institution   = {IPD, {U}niversit\"at {K}arlsruhe},
  year          = 1999,
  type =         {Verifix Working Paper},
  number =       "[Verifix/UKA/15]",
  verifixkey =   {UKA-VR},
  file          = {WhileCompile},
}

@Unpublished{	  HeberleGaul:GIF:98,
  author	= {A. Heberle and T. Gaul},
  title		= {{Syntax einer Sprache zur textuellen Repr{\"a}sentation
		  von Graphen}},
  institution	= {University of Karlsruhe},
  year		= {1998},
  note		= {{Interner Bericht}},
  verifixkey    = {UKA-Intern},
  file          = {graphsyntax}
}

@Unpublished{Zimmer-et-al:99,
  author        = {Wolf Zimmermann and Andreas Heberle and Wolfgang Goerigk},
  title         = {{The Verifix Approach Towards the Construction of
                  Correct Compilers}}, 
  year          = 1999,
  note          = {Working Paper},
  verifixkey    = {UKA-VR},
  file          = {fm99}
}


@TechReport{	  Dold96:Vx13,
  author	= {A. Dold and F.W. von Henke and H. Pfeifer and H. Rue{\ss}},
  title		= {Modelling abstract views on the Transputer in PVS},
  year		= {1996},
  institution   = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  type		= {Verifix Working Paper},
  number	= {[Verifix / Uni Ulm / 13.1]},
  month		= {Sept},
  verifixkey    = {ULM-Intern},
  file          = {abstraction}
}

@TechReport{	  Dold96b,
  author	= {Dold, Axel},
  title		= {{A Formalization of the Normalform Approach to
		  Compilation}},
  institution	= {Universit{\"a}t Ulm},
  year		= {1996},
  type		= {Verifix Working Paper},
  number	= {[Verifix / Uni Ulm / 9.1]},
  month		= {July},
  verifixkey    = {ULM-Intern},
  file          = {nf}
}

@TechReport{	  Dold+96d,
  author	= {Axel Dold},
  title		= {{Formalization and Verification of Code Generation
		  Rules}},
  institution	= {Universit{\"a}t Ulm},
  year		= {1996},
  type		= {Verifix Working Paper},
  number	= {[Verifix / Uni Ulm / 16.1]},
  month		= {July},
  verifixkey    = {ULM-Intern},
  file          = {local-rules}
}

@TechReport{	  Dold95c,
  author	= {Dold, Axel},
  title		= {{Representing the Alpha Processor Family using {\sc PVS}}},
  institution	= {Universit{\"a}t Ulm},
  year		= {1995},
  type		= {Verifix Working Paper},
  number	= {[Verifix / Uni Ulm / 4.1]},
  month		= {November},
  verifixkey    = {ULM-Intern},
  file          = {dec_alpha_pvs}
}

@TechReport{Dold98:Vx6.2,
  author        = {Axel  Dold},
  title         = {A Formal Representation of Abstract State Machines
                  using PVS}, 
  year          = {1998},
  institution   = {Universit{\"a}t Ulm},
  type          = {Verifix Working Paper},
  number        = {[Verifix / Uni Ulm / 6.2]},
  month         = {July},
  note          = {created December 95, revised July 98},
  verifixkey    = {ULM-VR},
  file          = {asm1_pvs}
}


% Pfeifer95:Vx3 = Pfeifer96a (???!!!!)
@TechReport{	  Pfeifer96a,
  author	= {Pfeifer, Holger},
  title		= {{Supporting Refinement Calculus Proofs in PVS}},
  institution	= {Universit\"at Ulm},
  type		= {{\it Verifix}\/-Arbeitsbericht},
  number	= {Verifix/Ulm/3.1},
  year		= {1996},
  month		= apr,
  verifixkey    = {ULM-Intern},
  file          = {refineproofs}
}

@Misc{		  Pfeifer96:Vx8,
  key		= {Pfeifer96:Vx8},
  author	= {H. Pfeifer},
  title		= {{F}ormal {S}pecification of the {T}ransputer {I}nstruction
		  {S}et in {PVS}},
  howpublished	= {Verifix Working Paper [Verifix / Uni Ulm / 8.2]},
  year		= {1996},
  verifixkey    = {ULM-Intern},
  file          = {transputer_pvs}
}


%
% Technische Berichte		  
%

% 
% Kiel, veroeffentlicht 		  
%		  

@TechReport{Goerigk/Hoffmann97,
  Author        = {Goerigk, Wolfgang and Hoffmann, Ulrich},
  Title         = {{The Compiling Specification from 
                    ComLisp to Executable Machine Code}},
  Type          = {Institutsbericht},
  Institution   = {Institut f\"ur Informatik, CAU},
  Number        = {Nr. 9713},
  Year          = 1998,
  Month         = dec,
  Address       = {Kiel},
  verifixkey    = {CAU-TR},
  file          = {CAU9713_Spezifikation}
}

@TechReport{Goerigk/Hoffmann98b,
  Author        = {Goerigk, Wolfgang and Hoffmann, Ulrich},
  Title         = {{Compiling ComLisp to Executable Machine Code:
                    Compiler Construction}},
  Type          = {Institutsbericht},
  Institution   = {Institut f\"ur Informatik, CAU},
  Number        = {Nr. 9812},
  Address       = {Kiel},
  Year          = 1998,
  Month         = oct,
  verifixkey    = {CAU-TR},
  file          = {CAU9812_Konstruktion}
}

		  
%		  
% Karlsruhe
%
		  
@techreport{heb_gles_loew_techrep1:1997,
	author = {Andreas Heberle and Sabine Glesner and Welf L\"owe},
	title = {{Names, Types, and Static Semantic Analysis}},
	institution = {{Universit\"at Karlsruhe}},
	year = 1997,
	type = {{Interner Bericht}},
	number = {13/97},
	month = {June},
	address = {{76128 Karlsruhe}},
  verifixkey    = {UKA-TR},
  file          = {StaticSA}
}

@techreport{gles_heb_loew_techrep2:1997,
	author = {Sabine Glesner and Andreas Heberle and Welf L\"owe},
	title = {{Generating Semantic Analysis  Using Constraint
		  Programming}},
	institution = {{Universit\"at Karlsruhe}},
	year = 1997,
	type = {{Interner Bericht}},
	number = {15/97},
	address = {{76128 Karlsruhe}},
	month = {June},
  verifixkey    = {UKA-TR},
  file          = {SA-CP}
}

@TechReport{BDvH+96,
  author = "F. Bartels and A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}",
  title = "{Formalizing Fixed-Point Theory in PVS}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1996",
  number =       "96-10",
  type = "Ulmer Informatik-Berichte",
  verifixkey    = {ULM-TR},
  file          = {fixpoints}
}

@TechReport{PDvHR96,
  author = "H. Pfeifer and A. Dold and F. W. v. Henke and H. Rue{\ss}",
  title = "{Mechanized Semantics of Simple Imperative Programming Constructs}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1996",
  number =       "96-11",
  type = "Ulmer Informatik-Berichte",
  verifixkey    = {ULM-TR},
  file          = {semantics-PDvHR96}
}

@TechReport{DvHPR96,
  author = "A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}",
  title = "{Generic Compilation Schemes for Simple Programming Constructs}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1996",
  number =       "96-12",
  type = "Ulmer Informatik-Berichte",
  verifixkey    = {ULM-TR},
  file          = {genericcompschemes}
}

@TechReport{DvHPR98,
  author = "A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}",
  title = "{Generic Compilation Schemes for Simple Programming Constructs}",
  institution   = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year          = "1998",
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Number        = {[Verifix/Ulm/10.2]},
  verifixkey    = {ULM-Intern},
  note          = "{revised version of TR 96-12}",
  file          = {generic-new}
}

@TechReport{Vialard99,
  author = "Vincent Vialard",
  title = "{A Library of Generic Compilation Schemes}",
  institution   = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year          = "1999",
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Number        = {[Verifix/Ulm/21.1]},
  verifixkey    = {ULM-Intern},
  file          = {}
}

@TechReport{Vialard99a,
  author = "Vincent Vialard",
  title = "{Local Verification of Parameterized Compilation Rules in a Limited Resource Environment}",
  institution   = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year          = "1999",
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Number        = {[Verifix/Ulm/22.1]},
  verifixkey    = {ULM-Intern},
}


@TechReport{Hoffmann95a,
  Author        = {Hoffmann, Ulrich},
  Title         = {{\"Uberblick \"uber die \"Ubersetzung von der
                  Compiler-Implementierungssprache  {\sc ComLisp} in
                  den  Maschinencode TC des Transputers }},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.1},
  Year          = {1995},
  Month         = jun,
  verifixkey    = {CAU-VR},
  file          = {}
}

@TechReport{Hoffmann95b,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzerimplementierungssprache {\sc ComLisp}}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.2},
  Year          = {1995},
  Month         = jun,
  verifixkey    = {CAU-VR},
  file          = {}
}

@TechReport{Hoffmann95c,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzerzwischensprache Cop}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.3},
  Year          = {1995},
  Month         = jun,
  verifixkey    = {CAU-VR},
  file          = {}
}

@TechReport{Hoffmann95d,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die \"Ubersetzerzwischensprache {\sc intermediateC}}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.4},
  Year          = {1995},
  Month         = jun,
  verifixkey    = {CAU-VR},
  file          = {}
}

@TechReport{Hoffmann95e,
  Author        = {Hoffmann, Ulrich},
  Title         = {{Die Assemblersprache {\sc TASM} des Transputers}},
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {CAU Kiel},
  Number        = {Verifix/CAU/1.5},
  Year          = {1995},
  Month         = jun,
  verifixkey    = {CAU-VR},
  file          = {}
}

@Unpublished{DoldVialard99,
  author =       "Axel Dold and Vincent Vialard",
  title =        "{Formal Verification of a Compiler Backend Generic Checker Program}",
  year =         "1999",
  note =         "submitted to PSI99",
  verifixkey =   {ULM-sub},
  file          = {}
}

@TechReport{Dold98d,
  Author        = {Axel Dold},
  Title         = "{Correct Compiler Construction in PVS}",
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {Uni Ulm},
  Number        = {[Verifix/Uni Ulm/20.1]},
  Year          = {1998},
  Month         = oct,
  verifixkey    = {ULM-intern},
  file          = {CompilerPVS}
}

@TechReport{Dold99c,
  Author        = {Axel Dold},
  Title         = "{Formalization of ComLisp and SIL}",
  Type          = {{\it Verifix}\/-Arbeitsbericht},
  Institution   = {Uni Ulm},
  Number        = {Verifix/Uni Ulm/19.1},
  Year          = {1999},
  Month         = jan,
  verifixkey    = {ULM-intern},
  file          = {}
}

@TechReport{Wolf99a,
  Author        = {Andreas Wolf},
  Institution   = {CAU Kiel},
  Month         = feb,
  Number        = {Verifix/CAU/6.1},
  Title         = {{An Exercise in Compiler Verification Revisited -- 
                    Preserving Partial Correctness }},
  Type          = {Technical Report},
  Year          = {1999},
  file          = {awo-exercise}
}

@TechReport{Wolf99b,
  Author        = {Andreas Wolf},
  Institution   = {CAU Kiel},
  Month         = feb,
  Number        = {Verifix/CAU/6.2},
  Title         = {{The Adequacy of a Loop's Definition}},
  Type          = {Technical Report},
  Year          = {1999},
  file          = {awo-loop}
}


@TechReport{Hoffmann98c,
  author =       {Ulrich Hoffmann},
  title =        {{Proof Protocols for the Initial Fully Correct Compiler}},
  institution =  {Institut f\"ur Informatik, CAU},
  year =         1998,
  note =         {10 Volumes},
  address =      {Kiel},
}

@InProceedings{Mueller-Olm/Wolf99a,
  author =      {Markus M\"uller--Olm and Andreas Wolf},
  title =       {{On Excusable and Inexcusable Failures}},
  booktitle =   {Proceedings of the FM'99},
  note =        {submitted},
  year =        1999,
  verifixkey=   {CAU-SUB}
}


@TechReport{Goerigk99a,
  Author        = {Goerigk, Wolfgang},
  Title         = {{Avoiding Trojan Horses in Compiler Binaries}},
  Institution   = {CAU Kiel},
  Type          = {Technical Report},
  Number        = {Verifix/CAU/2.9},
  Note          = {In Preparation},
  Year          = {1999},
}

@TechReport{GHLZ:2000,
  Author        = {G. Goos and A. Heberle and W. Löwe and
                  W. Zimmermann}, 
  title         = {{On Modular Definitions and Implementations of
                  Programming Languages}},
  Institution   = {Universität Karlsruhe},
  Type          = {Technical Report},
  Number        = {},
  Note          = {accepted for ASM2000, technical report or LNCS publication},
  Year          = {2000},
}

@TechReport{RSatherK:2002,
  Author        = {The VERIFIX Project}, 
  title         = {{R-Sather-K, The Language}},
  Institution   = {Universität Karlsruhe},
  Type          = {Technical Report},
  Year          = {2002},
}