Index: papers/FDL2012/FDL2012.aux
===================================================================
--- papers/FDL2012/FDL2012.aux	(revision 48)
+++ papers/FDL2012/FDL2012.aux	(revision 52)
@@ -42,26 +42,43 @@
 \citation{braunstein07ctl_abstraction}
 \@writefile{toc}{\contentsline {section}{\numberline {2} Our Framework}{2}{section.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.1} AKS generation from CTL Properties}{2}{subsection.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1} Overall Description of our methodology}{2}{subsection.2.1}}
 \citation{braunstein07ctl_abstraction}
 \citation{bara08abs_composant}
 \citation{ucberkeley96vis}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} CEGAR Loop}{3}{subsection.2.2}}
 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces  Verification Process }}{3}{figure.1}}
 \newlabel{cegar}{{1}{3}{Verification Process\relax }{figure.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{3}{section.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{3}{subsection.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} Definition of the abstraction of a component and of the complete system}{3}{subsection.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3} Characterization of AKS}{4}{subsection.2.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{4}{section.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{4}{subsection.3.1}}
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1} Refinement}{4}{subsubsection.3.1.1}}
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.2} The Counterexample}{4}{subsubsection.3.1.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{4}{subsection.3.2}}
-\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Example of weighting}}{5}{figure.2}}
-\newlabel{DepGraphWeight}{{2}{5}{Example of weighting\relax }{figure.2}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{5}{subsection.3.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{5}{subsection.3.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{5}{subsection.3.2}}
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Example of weighting}}{6}{figure.2}}
+\newlabel{DepGraphWeight}{{2}{6}{Example of weighting\relax }{figure.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{6}{subsection.3.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{6}{subsection.3.4}}
 \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.3}}
 \newlabel{AKSNegCex}{{3}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.3}{}}
-\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.4}}
-\newlabel{AKSNegCex}{{4}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{6}{section.4}}
-\@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{6}{section.5}}
 \bibstyle{IEEEbib}
 \bibdata{myBib}
+\bibcite{GrumbergLong91assume_guarantee}{1}
+\bibcite{HQR98assume_guarantee}{2}
+\bibcite{GrafSaidi97abstract_construct}{3}
+\bibcite{clarke00cegar}{4}
+\bibcite{XieBrowne03composition_soft}{5}
+\bibcite{PMT02compositional_MC}{6}
+\bibcite{SNBE06property_based}{7}
+\bibcite{microsoft04SLAM}{8}
+\bibcite{berkeley07BLAST}{9}
+\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{7}{figure.4}}
+\newlabel{AKSNegCex}{{4}{7}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{7}{section.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{7}{section.5}}
+\@writefile{toc}{\contentsline {section}{\numberline {6} References}{7}{section.6}}
+\bibcite{Kroening_al07vcegar}{10}
+\bibcite{pwk2009-date}{11}
+\bibcite{Kunz_al11ipc_abs}{12}
+\bibcite{braunstein07ctl_abstraction}{13}
+\bibcite{bara08abs_composant}{14}
+\bibcite{ucberkeley96vis}{15}
