Changeset 95 for papers

Timestamp:

Apr 10, 2012, 5:18:01 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

Location:

papers/FDL2012

Files:

• FDL2012.tex (modified) (1 diff)
• introduction.tex (modified) (2 diffs)

papers/FDL2012/FDL2012.tex

@@ -107 +107 @@
 
 %footnote for Table 1
-\footnotetext[1]{Computed on a calculation server.}
+\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
 
 %\begin{thebibliography}

papers/FDL2012/introduction.tex

@@ -21 +21 @@
 
 
+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.
+
+
 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. 
 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 @@
 
 
-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.