source: papers/FDL2012/FDL2012.aux @ 52

\relax 
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\catcode`:\active
\catcode`;\active
\catcode`!\active
\catcode`?\active
\citation{GrumbergLong91assume_guarantee}
\citation{HQR98assume_guarantee}
\select@language{american}
\@writefile{toc}{\select@language{american}}
\@writefile{lof}{\select@language{american}}
\@writefile{lot}{\select@language{american}}
\@writefile{toc}{\contentsline {section}{\numberline {1} Introduction}{1}{section.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1} Related Works}{1}{subsection.1.1}}
\citation{GrafSaidi97abstract_construct}
\citation{clarke00cegar}
\citation{XieBrowne03composition_soft}
\citation{PMT02compositional_MC}
\citation{SNBE06property_based}
\citation{microsoft04SLAM}
\citation{berkeley07BLAST}
\citation{Kroening_al07vcegar}
\citation{pwk2009-date}
\citation{Kunz_al11ipc_abs}
\citation{braunstein07ctl_abstraction}
\citation{bara08abs_composant}
\citation{clarke00cegar}
\citation{braunstein07ctl_abstraction}
\@writefile{toc}{\contentsline {section}{\numberline {2} Our Framework}{2}{section.2}}
\@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{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces  Verification Process }}{3}{figure.1}}
\newlabel{cegar}{{1}{3}{Verification Process\relax }{figure.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}{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}{}}
\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}