--- a/document/root.bib	Fri Jan 04 13:10:30 2013 +0000
+++ b/document/root.bib	Fri Jan 04 22:49:02 2013 +0000
@@ -42,4 +42,15 @@
   title     = {{C}omputability and {L}ogic (2.~ed.)},
   publisher = {Cambridge University Press},
   year      = {1987}
-}
\ No newline at end of file
+}
+
+@inproceedings{WuZhangUrban11,
+  author    = {C.~Wu and X.~Zhang and C.~Urban},
+  title     = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions
+               ({P}roof {P}earl)},
+  booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},
+  year      = {2011},
+  pages     = {341--356},
+  series    = {LNCS},
+  volume    = {6898}
+}