%PDF-1.5 % 4 0 obj << /S /GoTo /D (chapter.1) >> endobj 7 0 obj (Introduction) endobj 8 0 obj << /S /GoTo /D (section.1.1) >> endobj 11 0 obj (Automatic program analysis and verification) endobj 12 0 obj << /S /GoTo /D (section.1.2) >> endobj 15 0 obj (Logical-based programming and program analysis) endobj 16 0 obj << /S /GoTo /D (subsection.1.2.1) >> endobj 19 0 obj (A running example: browsing a web site) endobj 20 0 obj << /S /GoTo /D (section.1.3) >> endobj 23 0 obj (Models for Order-Sorted First-Order Logic) endobj 24 0 obj << /S /GoTo /D (section.1.4) >> endobj 27 0 obj (Automatic generation of models) endobj 28 0 obj << /S /GoTo /D (section.1.5) >> endobj 31 0 obj (Plan of the thesis) endobj 32 0 obj << /S /GoTo /D (chapter.2) >> endobj 35 0 obj (Preliminaries) endobj 36 0 obj << /S /GoTo /D (section.2.1) >> endobj 39 0 obj (Order-Sorted First-Order Logic) endobj 40 0 obj << /S /GoTo /D (subsection.2.1.1) >> endobj 43 0 obj (Sorts and order-sorted signatures) endobj 44 0 obj << /S /GoTo /D (subsection.2.1.2) >> endobj 47 0 obj (Theories, Specifications and programs.) endobj 48 0 obj << /S /GoTo /D (subsection.2.1.3) >> endobj 51 0 obj (Structures, Satisfaction, Models) endobj 52 0 obj << /S /GoTo /D (subsection.2.1.4) >> endobj 55 0 obj (Derived Models) endobj 56 0 obj << /S /GoTo /D (section.2.2) >> endobj 59 0 obj (Convex Domains) endobj 60 0 obj << /S /GoTo /D (subsection.2.2.1) >> endobj 63 0 obj (Domains) endobj 64 0 obj << /S /GoTo /D (subsection.2.2.2) >> endobj 67 0 obj (Functions) endobj 68 0 obj << /S /GoTo /D (section.2.3) >> endobj 71 0 obj (Conditional Polynomial Constraints) endobj 72 0 obj << /S /GoTo /D (chapter.3) >> endobj 75 0 obj (Formal treatment of a verification problem) endobj 76 0 obj << /S /GoTo /D (section.3.1) >> endobj 79 0 obj (Defining the theory) endobj 80 0 obj << /S /GoTo /D (section.3.2) >> endobj 83 0 obj (Defining the model using convex domains) endobj 84 0 obj << /S /GoTo /D (subsection.3.2.1) >> endobj 87 0 obj (Domains for sorts) endobj 88 0 obj << /S /GoTo /D (subsection.3.2.2) >> endobj 91 0 obj (Interpretation of function symbols) endobj 92 0 obj << /S /GoTo /D (subsection.3.2.3) >> endobj 95 0 obj (Interpretation of predicate symbols) endobj 96 0 obj << /S /GoTo /D (subsection.3.2.4) >> endobj 99 0 obj (Derived theory) endobj 100 0 obj << /S /GoTo /D (subsection.3.2.5) >> endobj 103 0 obj (Specific Conditions for the Analysis) endobj 104 0 obj << /S /GoTo /D (chapter.4) >> endobj 107 0 obj (The AGES Tool) endobj 108 0 obj << /S /GoTo /D (section.4.1) >> endobj 111 0 obj (Internal structure and work flow) endobj 112 0 obj << /S /GoTo /D (section.4.2) >> endobj 115 0 obj (Input data and data format) endobj 116 0 obj << /S /GoTo /D (subsection.4.2.1) >> endobj 119 0 obj (MAUDE program syntax) endobj 120 0 obj << /S /GoTo /D (subsection.4.2.2) >> endobj 123 0 obj (Goal Definition and Format) endobj 124 0 obj << /S /GoTo /D (section.4.3) >> endobj 127 0 obj (A short user manual) endobj 128 0 obj << /S /GoTo /D (subsection.4.3.1) >> endobj 131 0 obj (Web Based Application) endobj 132 0 obj << /S /GoTo /D (subsection.4.3.2) >> endobj 135 0 obj (Console Application) endobj 136 0 obj << /S /GoTo /D (chapter.5) >> endobj 139 0 obj (Practical Implementation) endobj 140 0 obj << /S /GoTo /D (section.5.1) >> endobj 143 0 obj (Development Environment) endobj 144 0 obj << /S /GoTo /D (subsection.5.1.1) >> endobj 147 0 obj (Haskell Compiler) endobj 148 0 obj << /S /GoTo /D (subsection.5.1.2) >> endobj 151 0 obj (Cabal Installer) endobj 152 0 obj << /S /GoTo /D (subsection.5.1.3) >> endobj 155 0 obj (mu-term Framework) endobj 156 0 obj << /S /GoTo /D (subsection.5.1.4) >> endobj 159 0 obj (mu-term Initial Setup) endobj 160 0 obj << /S /GoTo /D (section.5.2) >> endobj 163 0 obj (Implementing AGES using mu-term) endobj 164 0 obj << /S /GoTo /D (subsection.5.2.1) >> endobj 167 0 obj (Maude Parser Module) endobj 168 0 obj << /S /GoTo /D (subsection.5.2.2) >> endobj 171 0 obj (Command Line Interface Parameters) endobj 172 0 obj << /S /GoTo /D (section.5.3) >> endobj 175 0 obj (New Modules) endobj 176 0 obj << /S /GoTo /D (subsection.5.3.1) >> endobj 179 0 obj (Goal Parser) endobj 180 0 obj << /S /GoTo /D (subsection.5.3.2) >> endobj 183 0 obj (Generating convex domains) endobj 184 0 obj << /S /GoTo /D (subsection.5.3.3) >> endobj 187 0 obj (Generating Polynomial Interpretations) endobj 188 0 obj << /S /GoTo /D (subsection.5.3.4) >> endobj 191 0 obj (Specialization of the input specification using the inference rules) endobj 192 0 obj << /S /GoTo /D (subsection.5.3.5) >> endobj 195 0 obj (Final Transformations and Solver Execution) endobj 196 0 obj << /S /GoTo /D (section.5.4) >> endobj 199 0 obj (SMT Solver) endobj 200 0 obj << /S /GoTo /D (chapter.6) >> endobj 203 0 obj (Conclusions and Future Work) endobj 204 0 obj << /S /GoTo /D (section.6.1) >> endobj 207 0 obj (Conclusions) endobj 208 0 obj << /S /GoTo /D (section.6.2) >> endobj 211 0 obj (Future Work) endobj 212 0 obj << /S /GoTo /D (chapter*.23) >> endobj 215 0 obj (Bibliography) endobj 216 0 obj << /S /GoTo /D [217 0 R /Fit] >> endobj 223 0 obj << /Length 731 /Filter /FlateDecode >> stream xڕTn0+x%6i n/mLd1w%ʆ%.9;;kF dZJI$PYR@Uic