[48] | 1 | \relax |
---|
| 2 | \providecommand\HyperFirstAtBeginDocument{\AtBeginDocument} |
---|
| 3 | \HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined |
---|
| 4 | \global\let\oldcontentsline\contentsline |
---|
| 5 | \gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}} |
---|
| 6 | \global\let\oldnewlabel\newlabel |
---|
| 7 | \gdef\newlabel#1#2{\newlabelxx{#1}#2} |
---|
| 8 | \gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}} |
---|
| 9 | \AtEndDocument{\ifx\hyper@anchor\@undefined |
---|
| 10 | \let\contentsline\oldcontentsline |
---|
| 11 | \let\newlabel\oldnewlabel |
---|
| 12 | \fi} |
---|
| 13 | \fi} |
---|
| 14 | \global\let\hyper@last\relax |
---|
| 15 | \gdef\HyperFirstAtBeginDocument#1{#1} |
---|
| 16 | \providecommand\HyField@AuxAddToFields[1]{} |
---|
| 17 | \catcode`:\active |
---|
| 18 | \catcode`;\active |
---|
| 19 | \catcode`!\active |
---|
| 20 | \catcode`?\active |
---|
| 21 | \citation{GrumbergLong91assume_guarantee} |
---|
| 22 | \citation{HQR98assume_guarantee} |
---|
| 23 | \select@language{american} |
---|
| 24 | \@writefile{toc}{\select@language{american}} |
---|
| 25 | \@writefile{lof}{\select@language{american}} |
---|
| 26 | \@writefile{lot}{\select@language{american}} |
---|
| 27 | \@writefile{toc}{\contentsline {section}{\numberline {1} Introduction}{1}{section.1}} |
---|
| 28 | \@writefile{toc}{\contentsline {subsection}{\numberline {1.1} Related Works}{1}{subsection.1.1}} |
---|
| 29 | \citation{GrafSaidi97abstract_construct} |
---|
| 30 | \citation{clarke00cegar} |
---|
| 31 | \citation{XieBrowne03composition_soft} |
---|
| 32 | \citation{PMT02compositional_MC} |
---|
| 33 | \citation{SNBE06property_based} |
---|
| 34 | \citation{microsoft04SLAM} |
---|
| 35 | \citation{berkeley07BLAST} |
---|
| 36 | \citation{Kroening_al07vcegar} |
---|
| 37 | \citation{pwk2009-date} |
---|
| 38 | \citation{Kunz_al11ipc_abs} |
---|
| 39 | \citation{braunstein07ctl_abstraction} |
---|
| 40 | \citation{bara08abs_composant} |
---|
| 41 | \citation{clarke00cegar} |
---|
| 42 | \citation{braunstein07ctl_abstraction} |
---|
| 43 | \@writefile{toc}{\contentsline {section}{\numberline {2} Our Framework}{2}{section.2}} |
---|
| 44 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.1} AKS generation from CTL Properties}{2}{subsection.2.1}} |
---|
| 45 | \citation{braunstein07ctl_abstraction} |
---|
| 46 | \citation{bara08abs_composant} |
---|
| 47 | \citation{ucberkeley96vis} |
---|
| 48 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.2} CEGAR Loop}{3}{subsection.2.2}} |
---|
| 49 | \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Verification Process }}{3}{figure.1}} |
---|
| 50 | \newlabel{cegar}{{1}{3}{Verification Process\relax }{figure.1}{}} |
---|
| 51 | \@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{3}{section.3}} |
---|
| 52 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{3}{subsection.3.1}} |
---|
| 53 | \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1} Refinement}{4}{subsubsection.3.1.1}} |
---|
| 54 | \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.2} The Counterexample}{4}{subsubsection.3.1.2}} |
---|
| 55 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{4}{subsection.3.2}} |
---|
| 56 | \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Example of weighting}}{5}{figure.2}} |
---|
| 57 | \newlabel{DepGraphWeight}{{2}{5}{Example of weighting\relax }{figure.2}{}} |
---|
| 58 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{5}{subsection.3.3}} |
---|
| 59 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{5}{subsection.3.4}} |
---|
| 60 | \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.3}} |
---|
| 61 | \newlabel{AKSNegCex}{{3}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.3}{}} |
---|
| 62 | \@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.4}} |
---|
| 63 | \newlabel{AKSNegCex}{{4}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}} |
---|
| 64 | \@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{6}{section.4}} |
---|
| 65 | \@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{6}{section.5}} |
---|
| 66 | \bibstyle{IEEEbib} |
---|
| 67 | \bibdata{myBib} |
---|