Changeset 52 for papers/FDL2012/FDL2012.aux
- Timestamp:
- Mar 7, 2012, 5:10:31 PM (13 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.aux
r48 r52 42 42 \citation{braunstein07ctl_abstraction} 43 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}}44 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1} Overall Description of our methodology}{2}{subsection.2.1}} 45 45 \citation{braunstein07ctl_abstraction} 46 46 \citation{bara08abs_composant} 47 47 \citation{ucberkeley96vis} 48 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2} CEGAR Loop}{3}{subsection.2.2}}49 48 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Verification Process }}{3}{figure.1}} 50 49 \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}} 50 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2} Definition of the abstraction of a component and of the complete system}{3}{subsection.2.2}} 51 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3} Characterization of AKS}{4}{subsection.2.3}} 52 \@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{4}{section.3}} 53 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{4}{subsection.3.1}} 53 54 \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1} Refinement}{4}{subsubsection.3.1.1}} 54 55 \@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}}56 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{5}{subsection.3.2}} 57 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Example of weighting}}{6}{figure.2}} 58 \newlabel{DepGraphWeight}{{2}{6}{Example of weighting\relax }{figure.2}{}} 59 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{6}{subsection.3.3}} 60 \@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{6}{subsection.3.4}} 60 61 \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.3}} 61 62 \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 63 \bibstyle{IEEEbib} 67 64 \bibdata{myBib} 65 \bibcite{GrumbergLong91assume_guarantee}{1} 66 \bibcite{HQR98assume_guarantee}{2} 67 \bibcite{GrafSaidi97abstract_construct}{3} 68 \bibcite{clarke00cegar}{4} 69 \bibcite{XieBrowne03composition_soft}{5} 70 \bibcite{PMT02compositional_MC}{6} 71 \bibcite{SNBE06property_based}{7} 72 \bibcite{microsoft04SLAM}{8} 73 \bibcite{berkeley07BLAST}{9} 74 \@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{7}{figure.4}} 75 \newlabel{AKSNegCex}{{4}{7}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}} 76 \@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{7}{section.4}} 77 \@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{7}{section.5}} 78 \@writefile{toc}{\contentsline {section}{\numberline {6} References}{7}{section.6}} 79 \bibcite{Kroening_al07vcegar}{10} 80 \bibcite{pwk2009-date}{11} 81 \bibcite{Kunz_al11ipc_abs}{12} 82 \bibcite{braunstein07ctl_abstraction}{13} 83 \bibcite{bara08abs_composant}{14} 84 \bibcite{ucberkeley96vis}{15}
Note: See TracChangeset
for help on using the changeset viewer.