--- res/res.bib	2009/06/29 06:58:01	1.7
+++ res/res.bib	2009/06/29 09:28:41	1.8
@@ -1,4 +1,32 @@
 
+@article{781156,
+ author = {Lerner, Sorin and Millstein, Todd and Chambers, Craig},
+ title = {Automatically proving the correctness of compiler optimizations},
+ journal = {SIGPLAN Not.},
+ volume = {38},
+ number = {5},
+ year = {2003},
+ issn = {0362-1340},
+ pages = {220--231},
+ doi = {http://doi.acm.org/10.1145/780822.781156},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+
+@article{1040335,
+ author = {Lerner, Sorin and Millstein, Todd and Rice, Erika and Chambers, Craig},
+ title = {Automated soundness proofs for dataflow analyses and transformations via local rules},
+ journal = {SIGPLAN Not.},
+ volume = {40},
+ number = {1},
+ year = {2005},
+ issn = {0362-1340},
+ pages = {364--377},
+ doi = {http://doi.acm.org/10.1145/1047659.1040335},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+
  @article{1328444,
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
@@ -72,7 +100,10 @@
 @Misc{CompCert, 
   key = 	 {CompCert},
   author = 	 {Leroy, X.},
-  title = 	 {The Compcert verified compiler}},
+  title = 	 {The Compcert verified compiler.
+                  \url{http://compcert.inria.fr/doc/index.html}.
+                  CompCert is funded by ANR (grant number ANR-05-SSIA-0019), 
+                  as part of the ARA SSIA programme. }},
   howpublished = {\url{http://compcert.inria.fr/doc/index.html}},
   year = 	 {2005 - 2008},
   note = 	 {CompCert is funded by ANR (grant number ANR-05-SSIA-0019),