Changeset 95 for papers/FDL2012
- Timestamp:
- Apr 10, 2012, 5:18:01 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.tex
r93 r95 107 107 108 108 %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} 110 110 111 111 %\begin{thebibliography} -
papers/FDL2012/introduction.tex
r93 r95 21 21 22 22 23 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. 24 25 23 26 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. 24 27 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 37 35 38 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.37 39 38 40
Note: See TracChangeset
for help on using the changeset viewer.