Ignore:
Timestamp:
Mar 28, 2012, 6:10:10 PM (13 years ago)
Author:
cecile
Message:

ref SAT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/framework.tex

    r76 r77  
    1010generated and tested in the model-checker. As the abstract model is an
    1111over-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.
    12 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.
     12In this last case, the test of spurious counter-example is translated into a
     13SAT 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.
    1314
    1415%\bigskip
Note: See TracChangeset for help on using the changeset viewer.