diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 90f2893..7d73944 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -577,10 +577,31 @@ Algorithms Group, Inc., Downer's Grove, IL, USA and Oxford, UK, December 1992.
 Dunstan, Martin, Kelsey, Tom, Linton, Steve, Martin, Ursula
 ``Lightweight Formal Methods For Computer Algebra Systems''
 \verb|www.cs.st-andrews.ac.uk/~tom/pub/issac98.pdf|
+\bibitem[Dun97]{Dun97}
+Dunstand, U, Linton
+``Embedded Verification Techniques for Computer Algebra Systems''
+Grant citation GR/L48256 Nov 1, 1997-Feb 28, 2001
+\verb|www.cs.st-andrews.ac.uk/research/output/detail?output=ML97.php|
 \bibitem[Dun99]{Dun99}
 ``Formal Methods for Extensions to CAS''
 Dunstan, Martin, Kelsey, Tom, Martin, Ursula, and Linton, Steve, 
-FME 99, Toulouse, France, Sept 20-24, 1999
+FM 99, Toulouse, France, Sept 20-24, 1999, p1758-1777
+\bibitem[Dun99a]{Dun99a}
+Dunstan, MN
+``Larch/Aldor - A Larch BISL for AXIOM and Aldor''
+PhD Thesis, 1999
+\verb|www.cs.st-andrews.uk/files/publications/Dun99.php|
+\verb|axiom-portal.newsynthesis.org/refs/articles/mnd-sep99-thesis.pdf|
+\bibitem[DGKM01]{DGKM01}
+Dunstan, Martin, Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Computer Algebra meets Automated Theorem Proving: A Maple-PVS Interface''
+TPHOLS 2001, Edinburgh
+\verb|www.cs-st-andrews.ac.uk/~tom/pub/tphols.ps|
+\bibitem[DGKM01a]{DGKM01a}
+Dunstan, Martin, Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Computer Algebra meets Automated Theorem Proving: A Maple-PVS Interface''
+Calculemus 2001, Siena
+\verb|www.cs-st-andrews.ac.uk/~tom/pub/dunstanetal.ps|
 \bibitem[Du95]{Du95}
 Duval, D. ``Evaluation dynamique et cl\^oture alg\'ebrique en Axiom''. 
 Journal of Pure and Applied Algebra, no99, 1995, pp. 267--295.
@@ -640,6 +661,15 @@ material and energy balance concepts''. In Anonymous [Ano91], pp345-349
 V. Ellen Golden and M. A. Hussain, editors. Proceedings of the 1984 MACSYMA
 Users' Conference: Schenectady, New York, July 23-25, 1984, General Electric,
 Schenectady, NY, USA, 1984
+\bibitem[GKM05]{GKM05}
+Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Hidden verification for computational mathematics''
+Journal of Symbolic Computation, Vol39, Num 5, 2005
+\bibitem[BHGM04]{BHGM04}
+Boulton, Richard, Hardy, Ruth, Gottliebsen, Hanne, and Martin, Ursula
+``Design verification for control engineering''
+Proc Fourth International Conference on Integrated Formal Methods,
+April 2004
 \bibitem[GHK91]{GHK91}
 J. Grabmeier, K. Huber, and U. Krieger. ``Das ComputeralgebraSystem AXIOM
 bei kryptologischen und verkehrstheoretischen Untersuchungen des
@@ -807,6 +837,11 @@ Kelsey, Tom
 ``Formal specification of computer algebra''
 University of St Andrews, 6th April 2000
 \verb|www.cs.st-andrews.cs.uk/~tom/pub/fscbs.ps|
+\bibitem[Kel00b]{Kel00b}
+Kelsey, Tom
+``Formal specification of computer algebra'' (slides)
+University of St Andrews, Sept 21, 2000
+\verb|www.cs.st-andrews.cs.uk/~tom/pub/fscbstalk.ps|
 \bibitem[Kel99]{Kel99}
 Kelsey, Tom
 ``Formal Methods and Computer Algebra: A Larch Specification of AXIOM 
diff --git a/changelog b/changelog
index 8edcce1..6f213a0 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20111208 tpd src/axiom-website/patches.html 20111208.05.tpd.patch
+20111208 tpd books/bookvolbib add additional references
 20111208 tpd src/axiom-website/patches.html 20111208.04.tpd.patch
 20111208 tpd books/bookvol9 code cleanup
 20111208 tpd src/axiom-website/patches.html 20111208.03.tpd.patch
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 57e0f15..851ed6f 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -3733,5 +3733,7 @@ src/axiom-website/documentation update contributor list<br/>
 books/bookvol5 treeshake interpreter<br/>
 <a href="patches/20111208.04.tpd.patch">20111208.04.tpd.patch</a>
 books/bookvol9 code cleanup<br/>
+<a href="patches/20111208.05.tpd.patch">20111208.05.tpd.patch</a>
+books/bookvolbib add additional references<br/>
  </body>
 </html>