Changeset 95 for papers/FDL2012


Ignore:
Timestamp:
Apr 10, 2012, 5:18:01 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

Location:
papers/FDL2012
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/FDL2012.tex

    r93 r95  
    107107
    108108%footnote for Table 1
    109 \footnotetext[1]{Computed on a calculation server.}
     109\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
    110110
    111111%\begin{thebibliography}
  • papers/FDL2012/introduction.tex

    r93 r95  
    2121
    2222
     23Recently, 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.
     24
     25
    2326An 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.
    2427Several 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.
     
    3437
    3538
    36 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.
    3739
    3840
Note: See TracChangeset for help on using the changeset viewer.