--- res/res.bib	2009/06/26 07:34:20	1.4
+++ res/res.bib	2009/06/28 15:01:57	1.5
@@ -1,4 +1,4 @@
-@article{Hoare,
+@article{Hoare03,
  author = {Tony Hoare},
  title = {The verifying compiler: A grand challenge for computing research},
  journal = {Journal of the ACM},
@@ -12,7 +12,46 @@
  address = {New York, NY, USA},
  }
  
- @article{1328444,
+@inproceedings{TristanLeroy09,
+ author = {Jean-Baptiste Tristan and Xavier Leroy},
+ title = {Verified Validation of Lazy Code Motion},
+ booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
+ year = {2009},
+ isbn = {978-1-60558-392-1},
+ pages = {316--326},
+ location = {Dublin, Ireland},
+ doi = {http://doi.acm.org/10.1145/1542476.1542512},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+ 
+@inproceedings{Kundu+09,
+ author = {Sudipta Kundu and Zachary Tatlock and Sorin Lerner},
+ title = {Proving Optimizations Correct using Parameterized Program Equivalence},
+ booktitle = {PLDI '09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
+ year = {2009},
+ isbn = {978-1-60558-392-1},
+ pages = {327--337},
+ location = {Dublin, Ireland},
+ doi = {http://doi.acm.org/10.1145/1542476.1542513},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+ 
+@inproceedings{Necula00,
+ author = {George C. Necula},
+ title = {Translation Validation for an Optimizing Compiler},
+ booktitle = {PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation},
+ year = {2000},
+ isbn = {1-58113-199-2},
+ pages = {83--94},
+ location = {Vancouver, British Columbia, Canada},
+ doi = {http://doi.acm.org/10.1145/349299.349314},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ } 
+
+@article{TristanLeroy08,
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
  journal = {SIGPLAN Not.},
@@ -25,8 +64,76 @@
  publisher = {ACM},
  address = {New York, NY, USA},
  }
- 
- @article{1314860,
+
+@inproceedings{ZaksPnueli08,
+ author = {Anna Zaks and Amir Pnueli},
+ title = {Program Analysis for Compiler Validation},
+ booktitle = {PASTE '08: Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering},
+ year = {2008},
+ isbn = {978-1-60558-382-2},
+ pages = {1--7},
+ location = {Atlanta, Georgia},
+ doi = {http://doi.acm.org/10.1145/1512475.1512477},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+
+@inproceedings{Pnueli98b,
+ author = {Amir Pnueli and Michael Siegel and Eli Singerman},
+ title = {Translation Validation},
+ booktitle = {TACAS '98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems},
+ year = {1998},
+ isbn = {3-540-64356-7},
+ pages = {151--166},
+ publisher = {Springer-Verlag},
+ address = {London, UK},
+ }
+
+@Article{Pnueli98a,
+  author =	"Amir Pnueli and Ofer Shtrichman and Michael Siegel",
+  title =	"The {Code Validation Tool (CVT)}: Automatic
+		 verification of a compilation process",
+  journal =	"International Journal on Software Tools for Technology
+		 Transfer (STTT)",
+  volume =	"2",
+  number =	"2",
+  pages =	"192--201",
+  month =	 "December",
+  year = 	"1998",
+  ISSN = 	"1433-2779 (print), 1433-2787 (electronic)",
+}
+
+@article{GlesnerGoosZimmeermann04,
+  author    = {Sabine Glesner and
+               Gerhard Goos and
+               Wolf Zimmermann},
+  title     = {Verifix: Konstruktion und Architektur verifizierender {\"U}bersetzer
+               (Verifix: Construction and Architecture of Verifying Compilers)},
+  journal   = {it - Information Technology},
+  volume    = {46},
+  number    = {5},
+  year      = {2004},
+  pages     = {265-276},
+  ee        = {http://dx.doi.org/10.1524/itit.46.5.265.44799},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{GoosZimmermann00,
+  author    = {Gerhard Goos and Wolf Zimmermann},
+  title     = {Verifying Compilers and ASMs},
+  booktitle = {Abstract State Machines},
+  editor    = {Yuri Gurevich and
+               Philipp W. Kutter and
+               Martin Odersky and
+               Lothar Thiele},
+  year      = {2000},
+  pages     = {177-202},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1912},
+}
+
+@article{BlechPoetzsch07,
  author = {Jan Olaf Blech and Arnd Poetzsch-Heffter},
  title = {A Certifying Code Generation Phase},
  journal = {Electron. Notes Theor. Comput. Sci.},