diff --git a/doc/valviewer/tool_demo/p.tex b/doc/valviewer/tool_demo/p.tex
index 3698116950fcde375872b9d3fddcff65bdc00315..1dbea2d0fa2d8c881751529a5e739a1fcf2908b0 100644
--- a/doc/valviewer/tool_demo/p.tex
+++ b/doc/valviewer/tool_demo/p.tex
@@ -343,13 +343,15 @@ static analysis framework for the C language.
 In Frama-C, each static analysis technique,
 approach or idea can be implemented as a new plug-in, with the opportunity
 to obtain information from other plug-ins, and to leave the verification
-of difficult properties to other plug-ins which may be better adapted.
-The new plug-in may in turn provide access functions to the data
-it has computed.
+of difficult properties to other plug-ins which may be more fitted.
+%better adapted. Suggestion ?
+The new plug-in may in turn provide some access to the computed data.
+%access functions to the data
+%it has computed.
 The workability of the concept is corroborated by the list of
 existing plug-ins: value analysis, synthetic functional dependencies, program
 dependency graph, slicing (each of which builds upon the results
-of the previous ones), weakest precondition,\ldots
+of the previous ones), weakest precondition\ldots
 
 The value analysis of Frama-C is a plug-in based on abstract interpretation.
 It computes and stores supersets of possible values for all the variables
@@ -364,6 +366,25 @@ precondition plug-in) may pick up the gauntlet and verify the
 correctness of the operation for which the value analysis emits
 an alarm.
 
+As an example, we tried Frama-C on some of the Verisec test files \cite{verisec}.
+These files are C code from various real-life software sources (such as Apache, sendmail, etc.)
+where bugs have previously been detected and fixed. 
+The code source was reduced to a minimum slice of code,
+in order to perform relevant benchmarking of analysis tools.
+In most cases the bugs involved are about buffer overflowing.
+During this ongoing work, we were able to detect the expected bugs, 
+and sometimes more. 
+
+As an example, we show how a bug could be found in
+a C file extracted from the OpenSER source code. Though a declaration error
+can lead to the bug we expected, we found a more subtle error, 
+that only a value analysis could find. This result is achieved
+by running Frama-C for a first time in a fully automatic way,
+then, taking the emitted warnings into account, by providing some additional
+information about the analyzed program. Providing information can be done 
+by parametrizing the analysis or, if the code is partial,
+writing either annotations or C code to fill part of the blanks.
+
 \end{abstract}
 
 \begin{IEEEkeywords}
@@ -531,6 +552,11 @@ more thanks here
 H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
   0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.
 
+\bibitem{verisec}
+Kelvin Ku and Thomas E. Hart and Marsha Chechik and David Lie,
+\emph{A Buffer Overflow Benchmark for Software Model Checkers (Short Paper)}
+
+
 \end{thebibliography}