Changeset 77

Timestamp:

Mar 28, 2012, 6:10:10 PM (14 years ago)

Author:

cecile

Message:

ref SAT

File:

• papers/FDL2012/framework.tex (modified) (1 diff)

papers/FDL2012/framework.tex

@@ -10 +10 @@
 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