Index: papers/FDL2012/framework.tex
===================================================================
--- papers/FDL2012/framework.tex	(revision 76)
+++ papers/FDL2012/framework.tex	(revision 77)
@@ -10,5 +10,6 @@
 generated and tested in the model-checker. As the abstract model is an
 over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, if $\Phi$ holds on the the abstract model then it holds in the concrete model as well \cite{clarke94model}. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample, $\sigma$, given by the model-checker has been analyzed.
-In this last case, the test of spurious counter-example is translated into a SAT problem \TODO{citer ref SAT spurious}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
+In this last case, the test of spurious counter-example is translated into a
+SAT problem as in \cite{clarke00cegar}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
 
 %\bigskip