%PDF-1.5
%
1 0 obj
<<
/Metadata 2 0 R
/Outlines 3 0 R
/Pages 4 0 R
/Type /Catalog
>>
endobj
5 0 obj
<<
/Author (Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg)
/CreationDate (D:19700101000001Z)
/Creator (LaTeX with acmart 2018/04/14 v1.53 Typesetting articles for the Association for Computing Machinery and hyperref 2017/03/14 v6.85a Hypertext links for LaTeX)
/Keywords (Abstract Interpretation, Soundness)
/ModDate (D:20191217105757+01'00')
/PTEX.Fullbanner (This is pdfTeX, Version 3.14159265-2.6-1.40.18 \(TeX Live 2017/NixOS.org\) kpathsea version 6.2.3)
/Producer (pdfTeX-1.40.18)
/Subject (- Software and its engineering -> Automated static analysis; - Theory of computation -> Proof theory; )
/Title (Compositional Soundness Proofs of Abstract Interpreters)
>>
endobj
2 0 obj
<<
/Length 4206
/Subtype /XML
/Type /Metadata
>>
stream
pdfTeX-1.40.18
Abstract Interpretation, Soundness
2019-12-17T10:57:57+01:00
1970-01-01T00:00:01Z
LaTeX with acmart 2018/04/14 v1.53 Typesetting articles for the Association for Computing Machinery and hyperref 2017/03/14 v6.85a Hypertext links for LaTeX
2019-12-17T10:57:57+01:00
uuid:a57c7c71-ca6b-11f3-0000-fbe3b11c93d8
uuid:81534e47-415a-4898-8513-8432a92bd32e
application/pdf
Compositional Soundness Proofs of Abstract Interpreters
Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg
- Software and its engineering -> Automated static analysis; - Theory of computation -> Proof theory;
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/NixOS.org) kpathsea version 6.2.3
endstream
endobj
3 0 obj
<<
/Count 18
/First 6 0 R
/Last 7 0 R
/Type /Outlines
>>
endobj
4 0 obj
<<
/Count 27
/Kids [8 0 R 9 0 R 10 0 R 11 0 R 12 0 R 13 0 R 14 0 R 15 0 R 16 0 R 17 0 R
18 0 R 19 0 R 20 0 R 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R
28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R]
/Type /Pages
>>
endobj
6 0 obj
<<
/Dest [9 0 R /Fit]
/Next 35 0 R
/Parent 3 0 R
/Title (Abstract)
>>
endobj
7 0 obj
<<
/Dest [32 0 R /Fit]
/Parent 3 0 R
/Prev 36 0 R
/Title (References)
>>
endobj
8 0 obj
<<
/Contents 37 0 R
/Type /Page
/Resources <<
/Font <<
/F1 38 0 R
>>
/XObject <<
/Xf1 39 0 R
>>
>>
/Annots [40 0 R 41 0 R]
/Parent 4 0 R
/MediaBox [0 0 595 842]
>>
endobj
9 0 obj
<<
/Annots [42 0 R 43 0 R 44 0 R 45 0 R 46 0 R 47 0 R 48 0 R 49 0 R 50 0 R 51 0 R]
/Contents [52 0 R 53 0 R 54 0 R 55 0 R 56 0 R 57 0 R 58 0 R 59 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 60 0 R
/Font 61 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi0 62 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
10 0 obj
<<
/Annots [63 0 R 64 0 R]
/Contents [65 0 R 66 0 R 67 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 68 0 R
/Font 69 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi1 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
11 0 obj
<<
/Annots [71 0 R 72 0 R 73 0 R 74 0 R 75 0 R 76 0 R]
/Contents [77 0 R 78 0 R 79 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 80 0 R
/Font 81 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi2 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
12 0 obj
<<
/Annots [82 0 R 83 0 R 84 0 R 85 0 R 86 0 R]
/Contents [87 0 R 88 0 R 89 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 90 0 R
/Font 91 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi3 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
13 0 obj
<<
/Annots [92 0 R]
/Contents [93 0 R 94 0 R 95 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 96 0 R
/Font 97 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi4 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
14 0 obj
<<
/Annots [98 0 R 99 0 R]
/Contents [100 0 R 101 0 R 102 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 103 0 R
/Font 104 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi5 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
15 0 obj
<<
/Annots [105 0 R 106 0 R 107 0 R 108 0 R 109 0 R 110 0 R 111 0 R 112 0 R 113 0 R 114 0 R
115 0 R]
/Contents [116 0 R 117 0 R 118 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 119 0 R
/Font 120 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi6 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
16 0 obj
<<
/Contents [121 0 R 122 0 R 123 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 124 0 R
/Font 125 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi7 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
17 0 obj
<<
/Annots [126 0 R 127 0 R 128 0 R 129 0 R]
/Contents [130 0 R 131 0 R 132 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 133 0 R
/Font 134 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi8 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
18 0 obj
<<
/Annots [135 0 R 136 0 R 137 0 R 138 0 R 139 0 R 140 0 R 141 0 R 142 0 R 143 0 R 144 0 R
145 0 R]
/Contents [146 0 R 147 0 R 148 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 149 0 R
/Font 150 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi9 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
19 0 obj
<<
/Annots [151 0 R 152 0 R 153 0 R 154 0 R 155 0 R 156 0 R 157 0 R 158 0 R 159 0 R]
/Contents [160 0 R 161 0 R 162 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 163 0 R
/Font 164 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi10 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
20 0 obj
<<
/Annots [165 0 R 166 0 R 167 0 R]
/Contents [168 0 R 169 0 R 170 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 171 0 R
/Font 172 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi11 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
21 0 obj
<<
/Annots [173 0 R 174 0 R 175 0 R 176 0 R 177 0 R 178 0 R 179 0 R 180 0 R 181 0 R 182 0 R
183 0 R]
/Contents [184 0 R 185 0 R 186 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 187 0 R
/Font 188 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi12 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
22 0 obj
<<
/Annots [189 0 R 190 0 R 191 0 R 192 0 R 193 0 R 194 0 R 195 0 R 196 0 R 197 0 R 198 0 R
199 0 R 200 0 R 201 0 R]
/Contents [202 0 R 203 0 R 204 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 205 0 R
/Font 206 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi13 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
23 0 obj
<<
/Annots [207 0 R 208 0 R 209 0 R 210 0 R 211 0 R 212 0 R 213 0 R 214 0 R 215 0 R]
/Contents [216 0 R 217 0 R 218 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 219 0 R
/Font 220 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi14 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
24 0 obj
<<
/Annots [221 0 R 222 0 R 223 0 R 224 0 R 225 0 R 226 0 R 227 0 R 228 0 R]
/Contents [229 0 R 230 0 R 231 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 232 0 R
/Font 233 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi15 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
25 0 obj
<<
/Annots [234 0 R 235 0 R 236 0 R 237 0 R 238 0 R 239 0 R 240 0 R 241 0 R 242 0 R 243 0 R
244 0 R 245 0 R 246 0 R 247 0 R 248 0 R 249 0 R 250 0 R 251 0 R 252 0 R 253 0 R
254 0 R 255 0 R 256 0 R 257 0 R 258 0 R]
/Contents [259 0 R 260 0 R 261 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 262 0 R
/Font 263 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi16 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
26 0 obj
<<
/Annots [264 0 R 265 0 R]
/Contents [266 0 R 267 0 R 268 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 269 0 R
/Font 270 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi17 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
27 0 obj
<<
/Annots [271 0 R 272 0 R 273 0 R 274 0 R 275 0 R 276 0 R 277 0 R 278 0 R 279 0 R 280 0 R
281 0 R 282 0 R 283 0 R 284 0 R 285 0 R 286 0 R 287 0 R 288 0 R 289 0 R 290 0 R
291 0 R 292 0 R]
/Contents [293 0 R 294 0 R 295 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 296 0 R
/Font 297 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi18 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
28 0 obj
<<
/Annots [298 0 R 299 0 R 300 0 R]
/Contents [301 0 R 302 0 R 303 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 304 0 R
/Font 305 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi19 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
29 0 obj
<<
/Annots [306 0 R 307 0 R 308 0 R 309 0 R 310 0 R 311 0 R 312 0 R 313 0 R 314 0 R 315 0 R
316 0 R 317 0 R 318 0 R 319 0 R 320 0 R 321 0 R 322 0 R 323 0 R]
/Contents [324 0 R 325 0 R 326 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 327 0 R
/Font 328 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi20 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
30 0 obj
<<
/Annots [329 0 R 330 0 R 331 0 R 332 0 R 333 0 R 334 0 R 335 0 R 336 0 R 337 0 R 338 0 R
339 0 R 340 0 R 341 0 R]
/Contents [342 0 R 343 0 R 344 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 345 0 R
/Font 346 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi21 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
31 0 obj
<<
/Annots [347 0 R 348 0 R 349 0 R 350 0 R 351 0 R 352 0 R 353 0 R 354 0 R]
/Contents [355 0 R 356 0 R 357 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 358 0 R
/Font 359 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi22 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
32 0 obj
<<
/Contents [360 0 R 361 0 R 362 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 363 0 R
/Font 364 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi23 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
33 0 obj
<<
/Contents [365 0 R 366 0 R 367 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 368 0 R
/Font 369 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi24 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
34 0 obj
<<
/Contents [370 0 R 371 0 R 372 0 R]
/CropBox [0 0 486 720]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 373 0 R
/Font 374 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi25 70 0 R
>>
>>
/Rotate 0
/Type /Page
>>
endobj
35 0 obj
<<
/Dest [9 0 R /Fit]
/Next 375 0 R
/Parent 3 0 R
/Prev 6 0 R
/Title (1 Introduction)
>>
endobj
36 0 obj
<<
/Dest [31 0 R /Fit]
/Next 7 0 R
/Parent 3 0 R
/Prev 376 0 R
/Title (A Desugaring of Arrow Pretty Notation)
>>
endobj
37 0 obj
<<
/Length 1306
/Filter /FlateDecode
>>
stream
xX[oV>"Mz٪tWJ/`PlUVԿos|`Jv6\gf!/۵|ٵ?Ecxij8v٫Ѹ1ናxc4=o>6nGb3>5vpY<6Oo*RNR}P3JJvӖaxXcC&|>@B@B
AZAZZ-jO^%DhC5D/Lb;RNN3;pr1
A3 ?6(G}} + J Aˊ[4 =g^dA*_}
O98`\TV%ywW!<8CÜ\&DS6|0B}_>1n∬ O迀vZwΉe5V)#_BT:~M>x"T̛:2Kr8`~Y$]AkzwRg>UW5kK_MM ?\.XVvKWr^7Vx-
`p ,!HV1X
d4G<
{wPvSvCQ5r,S1G8콚=('t-$
_N[jjOddUX|)&0"⌌_ƥ|$)HS/KNDM}dTK\Ú9e9C*#Ť,3k?;#?n.Ov
:v0$kՊ8G~m\5
W8tvVДrXfC(@ {'>
oB9T=*e:3=g7t{Ki̿=t?
endstream
endobj
38 0 obj
<<
/Subtype /Type0
/Type /Font
/BaseFont /ZWHUZH+ArialUnicodeMS
/Encoding /Identity-H
/DescendantFonts [377 0 R]
/ToUnicode 378 0 R
>>
endobj
39 0 obj
<<
/Length 1732
/Subtype /Form
/Filter /FlateDecode
/Type /XObject
/Matrix [1 0 0 1 0 0]
/FormType 1
/Resources <<
/ColorSpace <<
/Cs1 [/ICCBased 379 0 R]
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/Gs1 380 0 R
/Gs2 381 0 R
>>
/Font <<
/TT2 382 0 R
>>
>>
/BBox [0 0 595 842]
>>
stream
xˎ^5)6om uxQd_+e6T[5|
_C.F=|KG=,u)nz5|xzsx~wiVb=?=qz8zȣINC}@>ȟfLmgR(ߊtkM9ڣu=^/l)GK I