diff --git a/document/introduction.tex b/document/introduction.tex
index 820a34e..c3cd40a 100644
--- a/document/introduction.tex
+++ b/document/introduction.tex
@@ -28,7 +28,7 @@ to express access control policies on the network level using a
 combinator-based language that is close to textbook-style
 specifications of firewall rules. To actually test the implementation
 as well as the configuration of a firewall, we use
-HOL-TestGen~\cite{brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012}
+HOL-TestGen~\cite{brucker.ea:interactive:2005,brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012}
 to generate test cases that can be used to validate the compliance of
 real network middleboxes (e.g., firewalls, routers). In this document,
 we focus on the Isabelle formalization of network access control
diff --git a/document/root.bib b/document/root.bib
index ea316ba..4c125f6 100644
--- a/document/root.bib
+++ b/document/root.bib
@@ -397,4 +397,40 @@
   isbn          = {978-1-4503-0688-1},
 }
 
+@InCollection{    brucker.ea:interactive:2005,
+  keywords      = {symbolic test case generations, black box testing, white
+                  box testing, theorem proving, interactive testing},
+  abstract      = {\testgen is a test environment for specification-based
+                  unit testing build upon the proof assistant Isabelle/\acs{hol}\@.
+                  While there is considerable skepticism with regard to
+                  interactive theorem provers in testing communities, we
+                  argue that they are a natural choice for (automated)
+                  symbolic computations underlying systematic tests. This
+                  holds in particular for the development on non-trivial
+                  formal test plans of complex software, where some parts of
+                  the overall activity require inherently guidance by a test
+                  engineer. In this paper, we present the underlying methods
+                  for both black box and white box testing in interactive
+                  unit test scenarios. \testgen can also be understood as
+                  a unifying technical and conceptual framework for
+                  presenting and investigating the variety of unit test
+                  techniques in a logically consistent way. },
+  location      = {Edinburgh},
+  author        = {Achim D. Brucker and Burkhart Wolff},
+  booktitle     = {Formal Approaches to Testing of Software},
+  language      = {USenglish},
+  publisher     = pub-springer,
+  series        = s-lncs,
+  number        = 3997,
+  doi           = {10.1007/11759744_7},
+  isbn          = {3-540-25109-X},
+  editor        = {Wolfgang Grieskamp and Carsten Weise},
+  project       = {\acs{csfmdos}},
+  title         = {Interactive Testing using \testgen},
+  classification= {workshop},
+  areas         = {formal methods, software},
+  categories    = {holtestgen},
+  year          = 2005,
+  public        = {yes},
+}