Index: /papers/FDL2012/FDL2012.tex
===================================================================
--- /papers/FDL2012/FDL2012.tex	(revision 94)
+++ /papers/FDL2012/FDL2012.tex	(revision 95)
@@ -107,5 +107,5 @@
 
 %footnote for Table 1
-\footnotetext[1]{Computed on a calculation server.}
+\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
 
 %\begin{thebibliography}
Index: /papers/FDL2012/introduction.tex
===================================================================
--- /papers/FDL2012/introduction.tex	(revision 94)
+++ /papers/FDL2012/introduction.tex	(revision 95)
@@ -21,4 +21,7 @@
 
 
+Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abstraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time.
+
+
 An alternative method to get over the state explosion problem is the compositional strategy. The strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. 
 Several works have manipulated this technique notably in \cite{GrumbergLong91assume_guarantee} where Grumberg and Long described the methodology using a subset of CTL in their framework and later in \cite{HQR98assume_guarantee} where Henzinger and al. presented their successful implementations and case study regarding this approach.
@@ -34,5 +37,4 @@
 
 
-Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abstraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time.