%PDF-1.5 % 1 0 obj << /S /GoTo /D (section.1) >> endobj 4 0 obj (Introduction) endobj 5 0 obj << /S /GoTo /D (section.2) >> endobj 8 0 obj (Motivating Examples) endobj 9 0 obj << /S /GoTo /D (subsection.2.1) >> endobj 12 0 obj (Control Flow Equivalence) endobj 13 0 obj << /S /GoTo /D (subsection.2.2) >> endobj 16 0 obj (Acceptability of Approximate Programs) endobj 17 0 obj << /S /GoTo /D (section.3) >> endobj 20 0 obj (Differential Program Verification) endobj 21 0 obj << /S /GoTo /D (subsection.3.1) >> endobj 24 0 obj (Simple Programming Language) endobj 25 0 obj << /S /GoTo /D (subsection.3.2) >> endobj 28 0 obj (Specification: Mutual Summaries) endobj 29 0 obj << /S /GoTo /D (subsection.3.3) >> endobj 32 0 obj (Modular Checking of Mutual Summaries) endobj 33 0 obj << /S /GoTo /D (subsubsection.3.3.1) >> endobj 36 0 obj (Product Programs) endobj 37 0 obj << /S /GoTo /D (subsubsection.3.3.2) >> endobj 40 0 obj (Adding Specifications) endobj 41 0 obj << /S /GoTo /D (subsection.3.4) >> endobj 44 0 obj (Invariant Inference) endobj 45 0 obj << /S /GoTo /D (section.4) >> endobj 48 0 obj (Control Flow Equivalence) endobj 49 0 obj << /S /GoTo /D (subsection.4.1) >> endobj 52 0 obj (Modeling Control Flow) endobj 53 0 obj << /S /GoTo /D (subsection.4.2) >> endobj 56 0 obj (Selection Sort Example) endobj 57 0 obj << /S /GoTo /D (section.5) >> endobj 60 0 obj (Acceptability of Approximate Programs) endobj 61 0 obj << /S /GoTo /D (subsection.5.1) >> endobj 64 0 obj (Approximate Memory and Data Type) endobj 65 0 obj << /S /GoTo /D (subsection.5.2) >> endobj 68 0 obj (Statistical Automatic Parallelization) endobj 69 0 obj << /S /GoTo /D (section.6) >> endobj 72 0 obj (Evaluation) endobj 73 0 obj << /S /GoTo /D (subsection.6.1) >> endobj 76 0 obj (Implementation) endobj 77 0 obj << /S /GoTo /D (subsection.6.2) >> endobj 80 0 obj (Experiments) endobj 81 0 obj << /S /GoTo /D (section.7) >> endobj 84 0 obj (Related Work) endobj 85 0 obj << /S /GoTo /D (section.8) >> endobj 88 0 obj (Conclusions) endobj 89 0 obj << /S /GoTo /D (section*.10) >> endobj 92 0 obj (References) endobj 93 0 obj << /S /GoTo /D (section*.11) >> endobj 96 0 obj (Appendix A: Product program details) endobj 97 0 obj << /S /GoTo /D (section*.13) >> endobj 100 0 obj (Appendix B: Control Flow Equivalence: C Benchmarks) endobj 101 0 obj << /S /GoTo /D [102 0 R /Fit] >> endobj 124 0 obj << /Length 4904 /Filter /FlateDecode >> stream xڅ[Kȑϯ`^&c}VY˶<w>T p P2@VUf*zU??16Anw$w$ۤcyrޟhƪۆk}Q}ߩ 3]+]=?yfnǺwj,%?ty=N},NqzyنfLp8cj˳WʿCD'ADfn&2ϧ軡ۍ2P8fyR[?H 7|^#rYcb8ܢ;}eDhDnYb_VOO7p0KJzG[X 9!&msXg%H"Fm=72X#b@MxIŇuL-$y4ȹGn\yrg> w80&*V&r73;lC1gھ[3R{#uhp1,p=Z`DTe{SZ"~l%%ѝ9(ũ(Q3pA:V4sSsTF,*s3:->[vX0vRsLQ,^J,ԓv5G+~XTg:[ޜѴd OJIM/~t ] Ʈz!4yiGLT_p|;lO/ eSHi ,EC[4 ]y>~<d挱F. xSv(F