\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} AKS generation from CTL Properties}{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 {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{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}