ࡱ> `!9*0Z0;2% $z'A$9xKIv#;{\b4 C"FEÀm(t {i/,ގ,e !V h0P`006 @oSzDa0[Je<##﫪lKrzܛ͌8'+NT猩01_y`͹I}_g;?>ÿG~[RE_}L?u;ߣwWgꃟkDo1?]|>`~_?Eoy튮^Uɵ)?S_}e=kg¿w5k/]Kw_?=bYܫ{?Ϳ7[{,i?%2Hc#x?}ϫ8~~d|b<*OƟO#C{GLxcN81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81NW.cJ]g )V #PE8%Ftz̥20~ i4#w'bTx`мa9 Wx _QF| 2hQ?7 0$ɽAɌ w;Y&6o0]\j`bx](뮣~)k\ʩy3 [W0b1/70 T2ݛ`0MݎC W껛70gqPbҽ>ؠ!N0F!_7}SΪB'9H,o/1$w1#%0FiCcޖ/;"`;Ő'ɗ23FU/Q V)v)S](3]`g_י_].!0|S¾ʂϾ5a;hUG-Pd.u@м6chW?N@~pa76O-HNZ7Au ud)ou4śe_aAz'(/w<`V;^(<x'$c]$ϱq1/j` Ëzhd&Jn)%~aa\5°Ġ zD_|ČI%5C߶ҟȊ̀I<|aQ ?ҳB(Ls73fd3FXZ a J"ux޼!pxFaG- Wܣeؚm/6emHngrH%W_AooA`mq=e8}9>8nZq{;粃)/}p\a%pOFlZh Lwa=1pȰٜ,ܓ`'s+`:PH=8?n ˄̂&JKjKLvaAsl9;:k"`-9@{gauҌ8::8#kZ _-X/&\fx2;GDԀcG YK䤱3A V3x4z3>:ubF;aݺ{1`|űNW],s{1bhW u~\ 4E4 "UR2e0 F32#HU*u܍AeU- ɒ5QH5 cXζ0Fsib.ƏPAhJ]p C@h#N@q" wcR_$T0H۩LPz8<ÖV'-^2.03˜*\E]unc`x< |ٸXOE*3xXMj+ܸU1I>F jW+j gUmXc{3æ>܁AvׁF`F3,LfT& Ψq&mzKpImbeAkBf8'Xr8&b`ʼ2>\%#ţWf#ƴ|ڙ ?v0&m&h;zpCPMc`Dd|'08iNn`xַ1z.LK ɸzAb\2WԔZLguP]:Tq3{3?K{ɋ~7, ?o0Nlp*`%?]pCQ3$."_ڻœ5wWҟ D%!Vŝ}Sǖ z9 -'/`\Z ǧ'#TX-ČN!a:O_Dl\p[Jc2 l)&*v M96-3꡻1(Uq5 NM`  ,\?Ա,!.xNcH)n9[M2)3pGU AVX~ G̋d9gVŒ\HฟU v)Ssi> aE dwc77D6H#xr `H+q0ȭ뛾I<0x 0}|;TKmcg1jH:\2 e*#w5na\Ej%2N1`lpoD+]bQ./orѰ7uXP))æ̌d{u"]J4 ]`3R13M80#Z&ca>;jI? C<%X1U~PUe#`55hlfWQ&9 |Nb-KR>`D ,!n b>XXQWfcR<΀[e{sG+.bPTz4˜U)z׻tAh\Ǯ7ljjK//󾠈,&㭌#dç0Mo&>Όg~% 2hbvl q]¹eQR Q긦:`$Ď%A 1B;ڎ0ipZKe-:OĨP arNL]μ1c4eyq 8=AP FԊn9dKjmP%o243 M>,r^28Ό+TحI%Vs> Xs֨eL>(J7%?yN.6\0)Rc4&M6 ?0ͱH?yuRER03Zu1ֻf53tR44F9d} >Gs]詉q֡+l. 9T99?'-I"Y$أsTQGRpuT0"3P&qiA2^2>*[ɩy"-l.0U+ЋqutXH1 g'C^S0&e b|NkAw Kh(9 ,R8fNM^mjJ \VJzT-ꔝm0 -ad^8 A)[Q <0dz |J^C`5ꦰp n;\ zTGKQ`ti~ `蕅m3d A5<Bl]ZTn4aNDvM@01TYiYӒB˾]%2j:A3MWîàoTg|1i>Apk!-46?3'o_kC6;bBFMRnd L]0-FP`$\t"Fl kVP`GױuȘ܊&y'gf(dd0} %sAG BXvhwdUՋ ݁ie:lnXPI_5^M,p.Jf< BSZѧHPUB/F0[;e=Ea/w ,AQHUsâYDUZ3eN]g{w>Dj #Ҡ ib@|Hz 6i74x[kZkE'f66il{nO>^F;-ȀOc:o ]Q/^jmn`d ߭5kH*_ n Uʊ&5ga)$= pIl thw] ub2h9 {CuLZs`LQ 0w0^;$-ل/j-0ÀQ||RSG;7FbPoq }Hӓ^wE= FP[˭݈OC1`Bg@r`n~ fc2 $fb֚*<WTmcUFN%Qqo3Q;ϩS 2#bb#ئe vU=MFU`Hp.(ڬ^3 $20hx7rF GjR_|1 @QE`tU|hѷ7ZFvCĀ44VJu7>Z}%"r$9.-XeE`%&pK}vf`NO&-1eƀ(Z#eiq%&#SAA:Qe*v $+`+1E`>Ȍkc 83 lI5ȕ.!"*# k;0"CJ̘l$e0e9gFq)yA/.Sbf5CVRڳ5Z+-{ETCQ)ЈKuVC PZ~nx"hB72ШZ[ԄflPT[/N_3Q&QGKdxԗ(l^Rid<t6lAeDxnӫU@aId} znihefjCvcؒ˒1q܎k'`)\*l缈`hdi,fF|Nn0c$ )\[:BC|*sМeh}R0_"d:DFG` F$0tlshv1ֺ4j-K 3kWeF%F2ж\+ 4h63b7[d2`LeEvȈXje]6(xދ x[w`weAmj CRA %*ce [*~R'b܈!;VUR+gxqS-wg Āφsw.6yf91ZѠ"^b `*hd2cT8MFd njH*J$m X)QDM9VʠZ7-Q 1^nr$ k;I m%U#+#TәݼO.{dm4 T,0Fa`{"I4-B8nEQQoypaha4 ᥩX+bKF0f[d .HzPdS^%?5^;',BȅQ]0ENsk'a F1k PQ@d`H|lt'AHŌ9u${uwv&wi 1D;&Kى0Y;/$O݂4YL'jH >R8{bumJh6:*ɡBRa7QB?#m2MIH{]S@^VVfWߵO./r~^|q'-vS_!pE݊dgEUh 3.-ok rN=mڋ..,NлdP pnNn㕘 9K} o0&dLu1Ʋ@Ŝ87M;.bc\/y QxeF3m}c/ܐ7zê0A,7Ƒr∯h/UQ7h}ESLQ1 FMMVW)J֬3lc؂1JBFkC>LECT9 }%6Pؿ; X%;/.ASɩ4>v PR φGJQnkVWbڔAu՘1j/GHUlp_kV+;MEQ};و^kQg38Gb 2GN7Y=AX5UMz稪ݷ- f 6"_͌d=}&UD<7ͺ BVWA') yt m+C߯G`Hm1م}/Eaי,s|wV2< t%넏! `L  k 2 3m dx |93aAdXW`;bc]fTwnN2wkca b^2$?`D>-^]ra[`Ki,;}ܝ65;3_~ F2zx|,7˂1lg y' #fm:/nS1xR21qgI`2-{Y4y$ud99plfE P0氽[g5/Դ!Gg]ۇpd8*H)lbX2sdf|'nY`>e߇ X1>|˹"z9H Đ`]du %PQ 0 ÌIy:#g‡2zTvwc oJ9*hpbC6,7j SzNvԔ #BK-e-kTZ>+ZtReAU|bRᎀu)J { ¬+(2/ Y%Ky 8]f+,ݦ;Bb, mNW#Șhգ:0i6q/G7_1^>d Ff6EN2w)FxlyCfCL1C2̀ sͥ 30ھ`}JTBfhS 2  ǝz%ѻ}hKFB2 18S'=Q fk"jqj(xhǩlg#犰˥wTfm2:SssLs0Ak 7h(q #R' ՠ`7jr3!K*gN0w;,sdJʅlgu\y%.NMXvCIq!X'>k4YG>Z؆p6V{Wlssl#`DVpՖ5JK&zIϞ'3N!VWJ1QV2k&fF/5fns_IS03ja*zF̾2ۙPq`3j-k$QF! :߽Ʌ~`h֔/vd47PcqRd~#30o QnYm0jEtZSȸ,,ю1 2'!QkYkq6?h>1YaP55 H鷁|t0`#ddnHAjdKY 6Wy%eH?5a*JGdX5A4N'mY?Ogpܫ {֏oq&7|V da?OV= D y6"C –6r0c ]j.4x`-ȹna:JFY2UI.axqV n~(VAS0(Dh@ 28bh_ijLčNg^^\VLKnJþ3Za}Gx3ʂaTiƒ] qtqWc;-ŹtGeƋYg,rXrr~qn%1:9dP#K>$S "FOKd`Q$}-wHmd8-jalLԙ SC AP#+p*9A gEsmdH.L]`-0Z:CpSfgp/>xBJVR㵕ȢV뙱ȥw "BjeFh° ]V1ZĐB(( mȇMF(szL_e0*Y3è Vu9u|NaVuxWհfB[$~k]ao7f(v1ڽ ܌lUJjt(-9y۬KxHၣ|t.agdlrM4@ ,gdaB"AƤ/1mqkiŒÓifw3 9d&r٫)S^o )h̀_͖v=m{o_Ƞg%֨u> ÌUG20AVӢdpˌ~1D0)հc/ ڕ:oJ6},7rEŌbn$R{: ~ށ2n0Pa}1#CMqQ)L<,ZaQf&xő`s K0:3tZ`OCA' 0Di$O ݅uPm6åUfF)D n<} OjfƢdyl"9廱"zp̬-59gp_jKU2MFn3Иy0VF_6| ?a1UsylA) s^MDd>l ),t`Ͱ&k&eCg#FU2̹VըgbN;30q02JO3#ɉYkdtZۂUݰ,wˌ -T뛂1'S+ALC6F-Y2fOk4u GA}V#mz"FVX2HƘcՒʗEl2Ga)+˒O4 6܍h2[YJTҾb2eFx]ΩJK֛V 9`hAt"=9e KHȆIĞ&^Dm}—Α\c`z;0_z:5xoja a1 AxĐ=ȣ ';3G~<#Dh/9X<1oX3koyDy>y2¡[0PL2EO8BngDNzqTT4-^ c GGn3.btס"jxl2Ue8 ;]ZW6R5#qCKlex(tr mr/0/idsuUȱWO ;adϙT([fwQ=It j11$JNH͍EV)vhۏq`50\fPdzj\1fz`F"\xq8;^-rt|!4Usz2 ?Ub_*~=!͌Kd`kF>1ghΒ0dL5acpԒ&jh_Fbx΍/yΟK9״F1W&yI RG5hͯw.=m2?zv੽| 3Tퟂ@&,Wy ѣIngzfGkť0uz"<593аvNTdc~VU:dt9QKIdCl;p Lu 7ufdFM͐tX8F܇hIyϷ3^䓑͚*9cޒj(_co'i2'uP_Mҟ?܁a0qb38W͌`4 R ;1\Gb|CK{(9ЫAQ-xtŚ7\vdnrM;O-2WY=G0lJV6oaߤV焫Kx^ì/S DW!O"%=1TO*q /|4ͥt$Kɧ깯/3S;,y?o+nμSqSߴ1p!uE^ɺWS>x!)[r|/Ë*x8jj^k!ga5C?UiÁ,,)+}l6vspVIMNR4' c5Q)fLlR8-uvڣKA.Qhw TcLף V9oo4 $i/# oYQثhS{3, #ylQX w-*Ac6' =b;B>r)dtsEQm~#[q %PUI>Fړ*j|u 2i?k]dXf`͏AmI#ߦ89wmǸo]9ZQk&j2 ˅j`v.853b(%6ľAL<0H'tP#aaJHǠaDރ-_(g1򱥭ASyB`<[}FFkHhgF5`ժ)K0<6>E8e0Z' USRvM0s 4Sb3oу?gx;cS%ߝoCiSJ60HJmE`f<>n41#HNU>F+ +񇤣(Vb P$~kȣ~9:W>##]W%nsͭ]0z0FCQ;(a& rlR`<ݯb YzfU'j.羊rȗIC1h-mOnc;mUd_q'vFKBHԒ7~ɲ]fU&|53m N8G!M T\H6^[ PjQk zj^oUKg,Rt6UU'bZ:^-+lYϤѾ S+G¨q,lj^os?|<״\ͧWw78~"_N[Yy;mo鏄'cE|j}A WBaX?Ӑ"80} }ք zM{k{+ݍoP] HtN6ʆTco"wcqO/]]R9V(jS118DsNA)ʘLQp1H SR  NX9QI)M p'|KswrԮArO~WޅAG.4Mr\ tHsҧdC4#=Mbƨe%3ƒs*c*u#6m]6IЌYƗ˓V:6l +ynOĠ9rr.63dԽ3 :.e cɑY1u%O:.*g'ƤOM:6U*kA/ۏwA5 ɯl܄_j2܏A2Â#A˺jѸ<:FdF_099HT̬ {9MA݅J~?hWV`ҽZ" dA cdˬ8{5ڄagFc͈ރ )erRa y2m3î1xuXɑ18F26yLc nou[cH\ߟ} XӔJ[}lsE'%mle,}.mҺ6A3)eФ|S :+-j/ch|oT#[vg_O ߭jKې37fyos*Up#o2Y|B7a ֛UL7amYvrR%s.0>2'@EM}3K<ٛ`47b1Zؚ:UyW|Cz?1|=عƝ~~Ax6),Om}[yo!֧X;7avFH clΪ>h;0Ȗ6FņFDF=z##g-WI8wb-G m5<ܝ1 28GĈ8"M=7GΌPI Eқdk7E2i!zR}ӌJ]ܙ{ͫc܋pF¶,#{2p<Vw$-~ F?tb'Ɖqb'Ɖqb:|+4:s:>Θk>ym˽n{'A BPNG  IHDR}{.gAMA|Q pHYs.#.#x?v{IDATH]n0 `N1A.2)G ;ƮnHb*EM 6+"]0}gw31wd5+@|hZ#A \b5 2HFь/9XG լQK}BD#xвEȯ3[ ?:|Am-V5,M 3nQt]QENa)ojMJuUeP -h^ИK'1XS Js`"I16ƚG` R[dhhh#/Vt{?Y;SR$X@-ǀNJjD&s&J@G_wќWBC%tsf(Ԡ."5Hu $ʡ(4 Ҹ{(,xx*E1xnQ7%gmzlch Q!+nxH^w:`=B_ /Eq!刽_ $3L6Do1譠5&z_`b 7!+|C/\Ok!WE3D~D{m|+{4 y҇Pq+Ծ?#> w:}qb Ǐ}YNWMdۿ>hg*DۤBSI WgNضC:⇐ f=4HԒuNYyK JԨ{= I+DqtnP9]v$bO𧚂T.) R= :B 3K - +JWDg0?[p~ԟR8 05p&,$ȎO\YBˬ(FA-; e4@?{|n{8*U92;R#_ks~yъFhA`nFL$\vKIENDB`T(@ |  -vPicture Word.Picture.80,Microsoft Word PictureN/ 0|DTimes New Roman0:A 0DComic Sans MSn0:A 0B Dcmsy10ans MSn0:A 0"0DArialans MSn0:A 0@DSymbolans MSn0:A 0 A 0(.2  @n?" dd@  @@`` | .  '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$$&"3,:U$$36F$#=(> NABCD!E GH8 JKAM!NOPQRST`$2$*0Z0;2% 9b${'A B9$$$$b$ st8%bm'; 0e0e     A@  A5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||s " 0e@        @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5%  N E5%  N F   5%    !"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab f3f3@ 57ʚ;I9ʚ;g4KdKd :A 0pp@ <4!d!dL$ 0{<4ddddL$ 0{<4ddddL$ 0{g4>d>d :A 0vp p2DEFAULTFONTSIZE10.DEFAULTWIDTH3540DEFAULTHEIGHT2000___PPT10 ? ,O =.w3Global Value Numbering using Random Interpretation43XSumit Gulwani George C. Necula CS Department University of California, BerkeleyY(1!2yGlobal Value NumberingrProblem To detect equivalences of expressions in a program To obtain a complete algorithm under the assumptions: Conditionals are non-deterministic Operators are uninterpreted F(e1,e2) = F (e1 ,e2 ) , F=F , e1=e1 , e2=e2 Existing algorithms Precise but expensive Efficient but imprecise Use randomization to obtain a precise, efficient but probabistically sound algorithm Complements our POPL  03 algorithm, which handles only arithmetictZjZ?Z.ZZ.ZVZBZj?                            .VBP #{S&OutlineTwo key ideas in the algorithm The affine join operation K-linear interpretations Correctness of the algorithm Termination of the algorithm63:3:%  2Review: Randomized Algorithm for Linear Arithmetic33 !Review: The Affine Join OperationDAffine combination of v1 and v2 w.r.t. weight w fw(v1,v2) w v1 + (1-w) v2 Affine join preserves common linear relationships (e.g. a+b=5) It does not introduce false relationships w.h.p. Unfortunately, non-linear relationships are not preserved (e.g. a (1+b) = 8) \04    > x.P  Uninterpreted Functions   e := y | F(e1,e2) Choose a random interpretation for F Non-linear interpretation E.g. F(e1,e2) = r1e12 + r2e22 Preserves all equivalences in straight-line code But not across join points Lets try linear interpretation6Ak A  N!(Nave) Linear InterpretationEncode F(e1,e2) = r1e1 + r2e2 Preserves all equivalences across a join point Introduces false equivalences in straight-line code    i"k-linear InterpretationsFEncode F(e1,e2) = R1e1 + R2e2 Every expression evaluates to a vector of length k R1 and R2 are random k k matrices 2k2 random variables, k = o(n) Works since matrix multiplication is not commutative e = R12(a) + R1R2(b) + R2R1(c) + R22(d) e = R12(a) + R1R2(c) + R2R1(b) + R22(d) Vw:R   3  :                3$The Random Interpreter R(OutlineTwo key ideas in the algorithm The affine join operation K-linear interpretations Correctness of the algorithm Termination of the algorithmB3:3 Completeness and soundness of R We compare the random interpreter R with a suitable abstract interpreter A R mimics A with high probability R is as complete as A R is (probabilistically) as sound as A&o?o?}The Abstract Interpreter A Completeness Theorem If S ) e1 = e2, then V(e1) = V(e2) Proof: Uninterpreted operators are modeled as linear functions The affine join operation preserves linear relationships +q  q  , eSoundness Theorem If S ) e1 = e2, then with high probability V(e1) V(e2) Error probability n: number of function applications d: size of set from which random values are chosen t : number of repetitions If n = 100, d 232, t = 5, then error probability :q"  V"'OutlineTwo key ideas in the algorithm The affine join operation K-linear interpretations Correctness of the algorithm Termination of the algorithmB3:3!Loops and Fixed Point Computation3The lattice of sets of equivalences has finite height n. Thus, the abstract interpreter A converges to a fixed point. Thus, the random interpreter R also converges (probabilistically) We can detect convergence by comparing the set of symbolic relationships implied by vectors in two successive iterations  Related WorkuEfficient but imprecise algorithms Congruence partitioning [Rosen, Wegman, Zadeck, POPL 88] Rewrite rules [Ruthing, Knoop, Steffen, SAS 99] - Balanced algorithms [Gargi PLDI 2002] Precise but inefficient algorithms Abstract interpretation on uninterpreted functions [Kildall 73] Affine join operation Random interpretation for linear arithmetic [Gulwani, Necula POPL 03]#i)$@F#!"$3   ,   C+K  R )Conclusion and Future WorkKey ideas in the paper f(e1,e2) = w e1 + (1-w) e2 Linearity , Preserves equivalences across a join point F(e1,e2) = R1 e1 + R2 e2 Vectors ) Introduce no false equivalence Random interpretation vs. deterministic algorithms Linear arithmetic O(n2) vs. O(n4) [POPL 2003] Uninterpreted functions O(n3) vs. O(n5 log n) [this talk] Future work Inter-procedural analysis using random interpretation Random interpretation for other theories Combining two random interpreters7)5#  ,          4         /TxP<  ` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@x?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>f-K0 bZ(    6 @  T Click to edit Master title style! !  00 0  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  0 `  @*   0    B*   0h    B* ~B  Hp?"@@H  0޽h ? ̙33 Default Design0 0 @(    Nr`r` )   x*  V++VV  Npr`r`  )  z*  V++VVd  c $ ?w  4  Nr`r`  ZF  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  T$r`r` @   x*  V++VV  TP%r`r`  @  z*  V++VVH  0~dm.F ? ̙3380___PPT10.47L P 0(    NYr`r` )   ^*  V++VV  Nr`r`  )  `*  V++VV  TԾr`r` @   ^*  V++VV  T4ar`r`  @  `*  V++VVH  0~dm.F ? ̙3380___PPT10.47Ui`5-K0 xp  (   x  c $,ڍ@  x  c $ݍ`    R  s *\; ; \h   s ,,3 A ??0  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B + k-K0 @ $(   r  S DZ@   r  S [`P  H  0޽h ? ̙33___PPT10i.v+D=' = @B + -K0 p $(  p r p S )@   r p S `0  H p 0޽h ? ̙33___PPT10i.0x)]+D=' = @B +Q0-K0 ,  `  (  `  ` 0XC"?`  "assert(x = y); assert(z = F(y));  #0 2#6 ` 6Ӎ @ Example  ` 6?"0@NNN?Nx ` @ 6?"0@NNN?NH X ` 0Pp ` <ؐ ?"6@ NNN?N0 =* 0 2   ` @ 6?"0@NNN?Npx ` 6?"0@NNN?NpH p ` @ 6?"0@NNN?NpP~ ` <y ?"6@ NNN?N +,$@ 0 nx = f(a,b) y = f(a,b) z = f(F(a),F(b)) F(y) = F(f(a,b))80 2              b ` 0 p ,$@ 0 BhTypical algorithms treat f as uninterpreted Hence cannot verify the second assertion The randomized algorithm interprets f Similar to the randomized algorithm for linear arithmetic,Z)Z&Z:Z)$:  ` 0$C"?P yx := a; y := a; z := F(a);  0 2  ` 0C"?p p  yx := b; y := b; z := F(b);  0 2H ` 0޽h ?_` ` `  ` ` ` ` ` ` ` ` ` ` `  33 : TIMING|39.3|36.4|44.5___PPT10."(+- Dv' = @B D1' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` ,%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` %(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` '%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` '8%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` ,U%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` U{%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` {%(+1) :-K0 @ 0 (  0 r 0 S ͗@    0 0ЗC"? Ka := 0; b := 1; 0 2 0 0җC"?  Ka := 1; b := 0; 0 2 0 0חC"? p  n2c := b  a; d := 1  2b; 0 2 0 0pۗC"?P P b&assert (c + d = 0); assert (c = a + 1) '0 2' 0 0ߗC"?   0c := 2a + b; d := b  2;60 2F  0 S 7WF  0 @ S YWL  0 @ c $?HX2  0 0 ;k F  0 @ S  d L 0 @ c $ HSPRB 0 s *DpRR 0 0(p  =T 0 2 0 00p  =T 0 2 0 0|p =F 0 2 0 0   =F 0 2R2 0 s *P0`F 0 S  B X 0 0?d 0 <GHW-I^ 0 6G޼HI޼X 0 00 d 0 <GHfI ^ 0 6GHI  0 s 0e0e    BC DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| bb|vTHT  | @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abj*,$D 0 0 H ?"6@ NNN?Np  ,$@ 0 Between random testing and abstract interpretation Choose random values for input variables Execute both branches Combine the values of a variable at join points using a random affine combination & 2z  p00 0  `@ P,$D 0B 0 HDjJ?"0@NNN?N p0B  0  HDjJ?"0@NNN?N p00H 0 0޽h ?@0 0 0 0 0 0 0 0 0 0 0 0 0 0 0  0 0 0 0 0 0 0 0 0  0 0 0  0 0 0  ̙33 8 TIMING|22.6|1.5|21.3 ___PPT10 .|0u+ogdD^ ' = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 3%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 3]%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 ]s%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 s%(+Q C-K0 `  (   x  c $d@@     c $4 <$@  0  " 0Pp  0iC"?` ,$@ 0 Ka := 2; b := 3; 0 2  0nC"? ,$@ 0 Ka := 4; b := 1; 0 2  6tr ,$@ 0 Da = f7(2,4) = -10 b = f7(3,1) = 15#0  z  S  ',$@ 0z  @ S 9 ',$@ 02  s *  @ P,$@ 0C  < 5 ?"6@ NNN?N P ,$ 0 e(w = 7)B0 2      H  0޽h ?/@    ̙338: TIMING|82.4|19.3|25.3___PPT10.v+ymD' = @B D}' = @BA?%,( < +O%,( < +D ' =%(DX ' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* e%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* "%(++0+  ++0+  ++0+  ++0+  +}--K0 &' 9(     0dNC"? Ka := 0; b := 1; 0 2  0PC"?  Ka := 1; b := 0; 0 2  0 C"? p  n2c := b  a; d := 1  2b; 0 2  0\C"?P P b&assert (c + d = 0); assert (c = a + 1) '0 2'  6X`0 @,$D 0 K a = -4, b = 5"0   6`d` ,$D 0 la = -4, b = 5 c = -39, d = 39 20  f  0iC"?   0c := 2a + b; d := b  2;60 2   6n`v ,$D 0 J a = 1, b = 0" 0     6r`P ,$@ 0 J a = 0, b = 1" 0     6v0 - ,$D 0 Ya = -4, b = 5 c = -3, d = 3"0 F   S 7WF   @ S YWL  @ c $?HX2  0 ;k F  @ S  d L  @ c $ HSPRB  s *DpRR  6|0  ,$@ 0 Za = -4, b = 5 c = 9, d = -9"0   0pp  =T 0 2  0xp  =T 0 2  0ćp =F 0 2  0   =F 0 2R2  s *P0`F  S  B X  0?d  <GHW-I^  6G޼HI޼X  00 d  <GHfI ^  6GHI    0T&,  hw1 = 5F0 2 ! 0&   iw2 = -3F0 2 " 6 @ #Review: Example $ H ?"6@ NNN?N  ,$@ 0  Choose a random weight for each join independently. All choices of random weights verify the first assertion Almost all choices contradict the second assertion  2F  p00 %  `@ PB & HDjJ?"0@NNN?N p0B '  HDjJ?"0@NNN?N p00H  0޽h ?@                                 33L TIMING0|25.7|7.8|19.3|10.2|23.4___PPT10."(+WxD$' = @B D' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ 5o%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ o%(+P+0+  ++0+  ++0+   ++0+   ++0+   ++0+  +  p-K0 P4 P(  4 r 4 S YP@    4 S 00<$@ 0  H 4 0޽h ? ̙33 & TIMING |37.3J ___PPT10* .}`1+ED ' = @B D ' = @BA?%,( < +O%,( < +D ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 9%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 :T%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 Tr%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 r%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(+VR -K0 , ((p#< &(  < r < S l@    j< <@° `   l k-  < k- ,$@ 0 l<  NDİ ?"6@ NNN?Nv AF$0 2   m<  Nǰ ?"6@ NNN?NmV  AF$0 2   n<  Nʰ ?"6@ NNN?N  AF$0 2   o< B <?"0@NNN?N p<  <?"0@NNN?N  q<  Bΰ?"0@NNN?N   Ca&0( 2   r<  BҰ?"0@NNN?N   Cb&0( 2  f3 s<  Bհ?"0@NNN?N   Cc&0( 2  f3 t<  Bذ?"0@NNN?NW -  Cd&0( 2   u< B <?"0@NNN?N   v<  <?"0@NNN?N R  w< B <?"0@NNN?NB   x<  <?"0@NNN?N   + y<  Nܰ ?"6@ NNN?Nk ge =H0 2      1 {< ND ?"6@ NNN?N ,$ 0 AF$0 2  1 |< N ?"6@ NNN?Ni ,$ 0 AF$0 2  1 }< N\ ?"6@ NNN?N ,$ 0 AF$0 2   ~< @ <?"0@NNN?N ,$@ 0 < <?"0@NNN?N  ,$@ 0! < B?"0@NNN?N  ,$ 0 Ca&0( 2  ! < B?"0@NNN?N  ,$  0 Cc&0( 2  f3! < B?"0@NNN?N  ,$  0 Cb&0( 2  f3! < B<?"0@NNN?N j @ ,$  0 Cd&0( 2   < @ <?"0@NNN?N + ,$@  0 < <?"0@NNN?N e ,$@  0 < @ <?"0@NNN?N U  ,$@ 0 < <?"0@NNN?N  ,$@ 0R < N ?"6@ NNN?N-,$ 0 b e =<0 2     < < ?"6@ NNN?N & ,$ 0 4 0 2   < H ?"6@ NNN?N [  ,$D 0 *E.g. e and e have same encodings even though e e Problem: too few random coefficients!Z[1 20      &   < < ?"6@ NNN?N  ,$@ 0 (Encodings e = r1(r1a+r2b) + r2(r1c+r2d) = r12(a)+r1r2(b)+r2r1(c)+r22(d) e = r12(a)+r1r2 (c)+r2r1(b)+r22(d) 0( 2q0 2                                                                                                                H < 0޽h ?%l< m< o< &l< n< p< 'm< q< u< (m< r< v< )n< s< w< *n< t< x< +{< |< ~< ,{< }< < -|< < < .|< < < /}< < < 0}< < <  ̙33)H TIMING,|29.5|18.9|7.4|6.|23.1a)___PPT10A).ff+%` D'' = @B D&' = @BA?%,( < +O%,( < +D' =%(D;' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*{< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*|< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*}< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*~< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =K@BBBBPB0B%(/%(#D' =1:Bvisible*o3>+B#style.visibility<*< %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< 5%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< -%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< -T%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< T{%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< 5[%(++0+{<  ++0+|<  ++0+}<  ++0+<  ++0+<  ++0+<  ++0+<  ++0+<  ++0+<  +: @+-K0 7@ ~(  @ r @ S d@    @ <e P<$@ 0  q @ Hhg ?"6@ NNN?N,$D  0  F(e1,e2)1b 0 2         q  @ H p ?"6@ NNN?N O,$@ 0  F(e1,e2)kb 0 2         5 !@ < w?"0@NNN?N P ,$ 0 ]e11>0( 2     "@ @ 6?"0@NNN?N% ,$@ 0 $@ @ 6?"0@NNN?N ,$@  0& '@ <,}?"0@NNN?N F ,$ 0 N& 00( 2   5 (@ <?"0@NNN?N & ,$ 0 ]e1k>0( 2    5 )@ <?"0@NNN?N J ,$ 0 ]e21>0( 2    & *@ <d?"0@NNN?N v ,$ 0 N& 00( 2   5 +@ <?"0@NNN?N & ,$ 0 ]e2k>0( 2     ,@ 6?"0@NNN?N% ,$@  0 -@ 6?"0@NNN?N% ,$@  0 .@ 6?"0@NNN?N%[ ,$@  0 /@ @ 6?"0@NNN?N ,$@ 0 0@ @ 6?"0@NNN?N  ,$@ 0 1@ 6?"0@NNN?N[ ,$@ 06 2@ H̗ ?"6@ NNN?Nv l ,$ 0 L& .0 2   H @ 0޽h ? @ !@ "@  @ !@ $@ @ (@ ,@ @ )@ -@ @ +@ .@  @ (@ /@  @ )@ 0@  @ +@ 1@  ̙337%B TIMING&|64.9|22.1|12.8|13.$___PPT10$.`]+1'^D#' = @B D"' = @BA?%,( < +O%,( < +D> ' =%(D ' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*!@ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*'@ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*(@ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*)@ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<**@ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*+@ %(Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*,@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*-@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ %(D ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*/@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*1@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* @ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*2@ %(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ !%(++0+!@  ++0+'@  ++0+(@  ++0+)@  ++0+*@  ++0++@  ++0+2@  +B' -K0 !@P (  P x P c $P@    P 0\C"?  B y := e 0 2 RB P s *Dpp P 6# p  NV100   P 6ҲS MV00  RB P s *D hhX  P 6ֲ6 xh  9*0   P 0۲ z  @True 0 2  P 0޲vp  AFalse 0 2X  P 0& d  P <G@HI@h  ^  P 6G]H*I]h 0  P 6hL MV00   P 6f   NV100   P 6P.   NV200  X2 P 00  ` F P @ S 9 d 7 L P c $`  F P S *K 7  P 6 D @ NV100   P 6 D + NV200   P 6@   MV00  B P HD?"0@NNN?NB P BD?"0@NNN?N  r P 0DC"? P ,$ 0 V1 = V[y V(e)]^0 2 ,B P BD?"0@NNN?N= .P 0@C"? 3c0,$ 0  V1 = V V2 = V`0 2   /P < ?"6@ NNN?NpPB +{V: Variables ! Vectors V(e): defined inductively as V(F(e1,e2)) = R1V(e1) + R2V(e2) Vj(e): the jth component of vector V(e)0|0 2    +                              \ :B 4P 6D?"0@NNN?N  =P 0C"? 9,$ 0 XJ Vj(y) = fw(V1 (y),V2(y)) for all y,j0 2 0( 2   , >P 0-C"? p 0g ,$ 0 Mj00 2 ?P 0H2C"? p 0 g ,$ 0 Mj00 2H P 0޽h ?_ P P  P P P P P P P P  ̙33 J TIMING.|72.5|14.6|26.8|6.5|3.8w ___PPT10W .v+D ' = @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*P %(Ds' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*=P %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*>P %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*?P %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*.P %(++0+P  ++0+.P  ++0+=P  ++0+>P  ++0+?P  + --K0 0x 0(  x x x c $E@   x x c $F0  H x 0޽h ? ̙33___PPT10i.0x)]+D=' = @B + g-K0 $ $(  $ r $ S M@   r $ S N0  H $ 0޽h ? ̙33___PPT10i.3+D=' = @B +  P-K0 RJ9 :(   x  c $hT@     6U(h 9*0   0T\bo\ @True 0 2  0\`b\ AFalse 0 2X  0kE d  <G@HI@BE ^  6G]H*I]B`   6pdrP8 MS00    6@i0 @  NS100    6m   NS200  X2  0] @F  @ S  L ! c $@u y F " S  d  ( 6r 8 NS100   ) 6w 3 NS200   * 6 | p  MS00  1 + 0hC"? P ,$@ 0 } S1 = S S2 = ST0 2        ! , 0܈C"?  ,$D 0 m1S = { e1=e2 | S1 ) e1=e2, S2 ) e1=e2 }  20 2         B - HD?"0@NNN?NJ()jB . BD?"0@NNN?N 0 0C"? 8( ,$ 0 JS1 = S[y /y] [ { y = e[y /y] }R&0 2  , 1 B\?"6@ NNN?Npp  SS: set of symbolic equivalences 2  2 0C"?Zx @y := e0 2RB 3 s *DZ 4 6  NS100   5 6 ( MS00  RB 6 s *D B 7 BD?"0@NNN?N  B 8 6D?"0@NNN?NH  0޽h ?_     "   !  ̙33 6 TIMING|17.7|13.6|8. ___PPT10 .v+T{DS ' = @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, 2%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*+ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*+ %(+8+0+0  + -K0  ( 0(  ( x ( c $H@   x ( c $00  H ( 0޽h ? ̙33___PPT10i.v+D=' = @B +  -K0   0,  (  , x , c $@   x , c $00  d ,  pA ?txp_fig"6@ NNN?N. p ~ SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $$\left(\frac{2n^2}{d}\right)^{t}$$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False*RESOLUTION300*TIMEOUT (none)&BOXWIDTH354(BOXHEIGHT200"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG FalseD*ALLOWFONTSUBSTITUTION False6BITMAPFORMATbmpmono.ORIGWIDTH 68.8756PICTUREFILESIZE8594B , @ 6D?"0@NNN?N(D ,  pA ?txp_fig"6@ NNN?N f^ SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $\frac{1}{2^{100}}$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False*RESOLUTION300*TIMEOUT (none)&BOXWIDTH354(BOXHEIGHT200"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG FalseD*ALLOWFONTSUBSTITUTION False6BITMAPFORMATbmpmono.ORIGWIDTH 37.8756PICTUREFILESIZE2562H , 0޽h ? ̙33___PPT10i.v+D=' = @B + ,-K0  t 0(  t x t c $@   x t c $H0  H t 0޽h ? ̙33___PPT10i.0x)]+D=' = @B + @$-K0 0 0(   x  c $,@   x  c $0  H  0޽h ? ̙33___PPT10i.v+D=' = @B + 0-K0  0(   x  c $@   x  c $lP0  H  0޽h ? ̙33___PPT10i.v+D=' = @B +. ;-K0 @| r(  | x | c $T@    | c $ p<$@ 0  "8XH | 0޽h ? ̙33. TIMING|50.1|32.___PPT10~.v+EDR' = @B D ' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| '%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| 'J%(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| JV%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| V%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| %(+ 0 0 +(   d  c $w     s * : ZF    H  0~dm.F ? ̙33% 0 zrh  (  h X h C w   r h S  ZF   H h 0~dm.F ? ̙3380___PPT10.P!! 0 zrl  (  l X l C w   r l S C ZF   H l 0~dm.F ? ̙3380___PPT10.@BESx\e]\nPRRZTDiFD)iXR@D=u{?gӍL#faX .>~pxxc5 _1}>)CgeTc@`0``@@p"1 )9%Չw΃0000\    p@@@@Ql@bRddTT p @@@6m]=}C#&fVX888<px ܭ:O@g~; |x/6(FC#' p%rM@`__=dQ~4qWOp8w*IeT!ہ 8FC:J4@gф6ߛЀE?w\~ %s#;k{k* kTFvG]M*)k |d%~І@_;X?ݿ6?zg߆ 94̟J ?YEs1!0-s5fDj+*ClGLg x!Oฝ:u tb2 PU:G*P,9Y)/FC=:א0W:׽wmn@Ŋ Nk՜G?'TʆD->y_HV#ξ$AFduiƇ}[ra<(hL抡.})): wyRK̩!^l)̒lEHn6  \Ǫ]4nɼh=U^'u Ǻ\FS2g#h\a.o{j-66 I$ &Ec׾iy^|fN9u{z,7[+%Czbj2[ĸ./`!˟LFuq! 'KD*q96yx:]1<7"ʸtV6 8:3N\H_Yy:7吾4IHJG $ܙB/>+.,8ΠvGǐ.MdZ tL3V+^̡ipWt\fT˻cӢVRb yECiw;uQptpmy?JF: n=~6bZ덐ވv"0"pt@ΒX C,ZWMdяp|=)/TErv8pa4#mP|7E6gxg_腽ؔ*ͺܕjo(|YC܄WiU3Y{]Yj2BP~u=;>HO Y.˿ zx.ԩBk&۾6GdU T.?y4 "o`=1 AlmѰR% *Op(.7 ٭q/uٛ3Q$ziU_ERDzR+8x?FȦ%w{)Nd"[u6A)P;lICU+!Dstl45sv`Yh0fÄ>,ǯe^L wDqp~򔪠X!)/j [62j'C%<\o\F侺xw`="{:H3ߗC&k|Z z"XrB81V~n[<ow@M!>g2r\|k`ϋDӳIp$3\/F=2 􌮩r7wՉ {Cw#X aZ~8OAPci;)1YW*Aо;y)RwD_4¥t]jC_Ј!I`'^gFT\8-.KI yc\jn7 2Q#_]lwKl<|2y~)LK&h|WW,%]U/ooD#wbkFc/u)5h'f@DS5gChuőL!TCW-]~!Y0xgGl*Vsk>^՘pL1:e Ǭ sro1<?;FK/@GXϦ&dں .AM{&[v;F|l}wH8\P rh;#CW:ƮPYs1XɺЧ3fJ5 vllaXx߿oV͔T pIs1 wŽ)BJ]/Pct\B=K#2IQ$ ^gB_C[NE ,IF4:8~6 lA~u.Tҡ {~/&,*׼G%_9Fx*BO珑݁q?B׽aQH-3E'Nʇ(w;p;Y'D} sSܯmvq7BgC>EKP;|}7B 9){ٛhYV-W'A Ek^-8eV7_eyF?gֹ&،D"+ǻ$#բ,r-"rDlD. `* 0K(d˖U{G1iη6٠Pu%7Q^;Ffv q0!-/zϦI զpp.)#k #ɭm3{kozG@S.1Ys'&fRq ,wq=YTOC_/d9US $ u؏]lI7& M6N8sńcO "- 7i[Qvy<.U)cgZaP&_t̰ք}D7>143PN/zLW" RAnG1\~pi!1gU+0 4,e8I)N=-~1Z(1=ܣ*2bNI;"Xt\%,0iI^^]Ͳͯ1rxlTҢPC>v4 CF8 uM+VY};FSn(_%9t Ƨ2V~/ o7>h&#-XŒڟk9;+ƭ*N^XY~*y؋8f)ixꓹ7`2r}Dy%!&h]$?Ht'X&\Sxh3i!kaG+YW'ov.f՘Okq\IS"dd[kC>L4q/gIRn+p65lvmW8ӦMq[wҺYoSϝ3>͞j;h530Yn A#|vk_dVE":?.Çxx4$#l|o]LN`jC"åj-,h %O/W&'-/Ţ{ QsćD-"M]Z1XfD^f DGr TεZvAvd0y6.e' Nw#[INYi w#p˙؊Eϫhv``i'rk0F.<%w0Wv_DAD3T1 ^\sfLV9LcGvArҹDwD_"AdY_"(˒HH<GGP}4ޭƆXek '.B/]٘z,jwmvpZz4Ne.%IEǥ݀n!>{zk>NoIS|k {-58>+h-DxOIB̄O%t&urKěϹ ݧ)&%Xxܙdf\~IGm kJ3fG }6϶/!n% +khH _#~)@C<~Ϯ4{++,W[l d Xt兆mvޒ.|1l7⮸Hr1 !NrRf c ax*LvǒO9gV=_Z?<v2U$rY JJ^\xd9mS#ezIJK!d ޿wrfkgZɓ T~{FL3o\Eypa1C2OTgÁZ G~xWI3v.[:vM( \r 8[RQxGIZ$,MוsmP l+;=M3W,`t `ַ2Ex$cjLxX*["GsH?>jCJ,ο{wskq]o6%ORbd{%٠켜p 5G/997)vK=YW ͛]5N5 #ڲ)CD[ll;0 Dl,ܝr_ {zxE]|}sNǼ]`6c Dxe"&Ɯw#^ ^֦6==ma~MUu !]eQcVzI,$s-a|L e4©;0#CYY1i=jc̋U>c!".v0a#[l8hH5/M|JLnƛl,4Yb_%ɂHZ!Jk/1TI\|M3džTʽjc`>iN;Ltq$M.c\Ѭ}Io;>Wׂ|dGv@Ha/6VHV-|@wa3JS 8 O%k]P~sm[ƓFoZ {JtJ~s^# obtB=K b2E^"ܮh/-ǮB5)UY7݅.?e y,k ꬐ũ/z(la*2]+3.4 PX"{A[._ ߱TVs k.h-bo]Xuff W- icQ'#Ч?ǻ~$ǜ-b$椴 5>ACؼ=>ra;hm,K,~c$$ -sDe5`AAȅ̂.id~IW9).@d'yvZLK郟f9B8^ߗ:3!vPRS|>NxcpИK/44TV`, L7+. 17N<Eh.Xv \ُ JO.D=ZPz'xZA;Y3vOw?^/`B\ @jmе^T΄AqKog+^l`Kt-)%ǚ`7\(K J [qeuTD<̛G 9ʹ\WI>ƏKw>d=j*L~toJA ֌)P ,Mis{>&'f]CD]X d"F7;l^Ey`/FY} Q_ ~AjA?"KY4\@1HPgtX1i!}7rg_mUje} 96~Eqf=0rԥ +phʀoe̻\x^+.3_0jĠ7SU#!M):EZ6=߁V8j/oޯ2ڨTHȉ>d"1(n^TD/^|Kmu*{wR(F-EMΧџϔS<1NOͷqR (}a 7<#\]ce{'bݫsBs> ng ŰEs-µky7b zi;~Q<OȶnL+XY7RޮȪ ֘ƺ+ƾRUɠ&Q>ՁƐ0{C"PG~1T;r7ޜֆ-m;}mḾC6g໼ԳRҋ]YxtT:0tM9f c /m.9*T;K]U,zAP.AMqc> p RC"4]GjKލW|vW88)F5g@D} ~5yϸO&?ȫ-ł)F/Ǵ]K0N'L㹝n[e\8"ڋ1۪#.4s&,hE:y?gcX꿔/"znso\T^7q=Qvfk2SK7p, s\FE)T AjӞ'g!5|x+Q&I(D U9-ֳ:ׂ.;R)_~_|֌_<" VtʈLp]F;ݺj%monE#C_ Zc\἟̃!-gj/ F_^θ _Gc:r~0a˼S%b0B3׶y5;cNƜ{Ũ@%ZKNy@+B3{אLt1")?ؐeRb׍L vbz 3ʉeo0L|Be$VNeƤ~n^'㫀eF^%K]XfpW?ֵ^ҰM(gGw(+qF]q?-Y2^0% }̐WG }P3^Em1*Kղz_&Qo|ʙzjYp Ӥ |F={1vjM=QkBC\pDq蔌]HBn5)J zmey>Yq ]u]eJ J8SZQg,ؓaęܳ3Bf6֎"槷x7Kp}Y HwjV)AKzGvJ$.IwqNsIjZԁjߚZt> z9ט:"!Jt<^\Z-£ wΔc\NmQoªsđ޽&5:e9V8:{W¬>rBqm\P1/I-q.L#XecE$Q ZR/ɵNvao)^QX8̎Y˻jlNb+Ț3p5}sz׉ѓBAVbZ0bk)kqap #aROWZryn X&`_0%cB9!UGFyޞ&[ńȼfK79g~W]-ʼ4o sK2ٹԼm>}hajHKAB*H|&eqNηOޜB<.u<;5^VȺ03ŏn t,]Nq3,c%1 M 6.='BO-bz=q#z-{od |JfJ'R˃ӽ98[ϺMF`OQ 2 Kvlb^ZѰeK":}aٓe2Ɗ_wF˱ֹ*;vhtިNv7WN*{|kQ+ : kqܵ!dDPmrr)Y廳˷27o;fLH][I:` u5\-dtD3A!bX-}>R)Q.P[jWOp$nEtY!Ug6A:c1"a>.zbbpOe(]8gfь`lYn؞hBna!K..~tsҶbZB^&&!ZI^4uM3ˌoeZ:ڷjRQ[RL& 6n2d?LYF ;1T0-FC9LTt=suWy_t39R@nY|*JDdЬWI\YfءYTg` ͐@l IqqK矸h=ܭnn^Obr IzZØZSSHse6E)簨ذXq=v - ҆yV1{hd4(=Rf^{tLYxC&6ġ>D`gxHW:t ZA%49Y- W$!_?=Ix Olp{u ZbnsJ~pCcq˥2BL䠱"s) >7v/7|0{ `D u>Xťd2oc<{RR,U\1U=Z/+:wIAsQ_oX7[&XXS}ajWG\W'V>MsaBH|.UfssF꘯HZyO,֒g!҄rț>r<}$i_xHS G__(daxw%w4$Mz?%:>0yZ|y-i;zzOiLUR/hrG/-e&~|~Z HN%[͆ Md];fpٍHnDYC/^,GCZ&nMV4 Z/lJWCà2|6+g/@J?%޺S9Y]2fEC݇[UhA,kW.ζ]v^od{ADκE:|&`IKQdNmexKz9p?Jm\ւcbTx/ƕ'˅nV*$oSJHM49: 5'K2HtC0F[_3SoGrĂ | #TTӱʑFu6؝ [D[^olqըdvo1X/Vx)uuo[pI&C2<(Xo{:&Ot߇wiOp P'=yۺ\BpǮ.KBd[~u,5~}Jr[`)g;]mlDDuШd_v̪/ fq]sF՚XK".9 Y$[D Y'Lnn Yekm){fؚg!֘*76VAw=iQ8dtW1oXtG})g-+{RM^J6%F5 `Ւ I6eud7f3#CuJ"h!v-[Ս'筸.A4b[18rU9*P!g;\e rxI4^lb*!mH8G){V]4>\]I! QߢIi՟r_`fsH 2*F'gf.?gh&5:mpas0Qz,Pf~_(h|Dc&f,GUT۵ )hptU \6TV|;-ߥtP?YO`k{ek3׈7J\DDe>Ê3H`xK}+yX\9KK]>I)*1P }|Ѥ];ރC%+s65\I^Bv^]=f r\9D8砌PmUN֡k}( ]#w`VQNMQ%3 H~~Ut0ax/V1#FGPW\p'sW|{/aE_&2*];Ղkϡ*|ql".L{f\2E7- vuT4m)΄XQ˹!&9$ߨVAGϪ']XVQ{Uf#%6 2&ͳJqR7&B\9jАICm0R̻QVY]B+B[S\X6yb+(Q]`v m=SƐxme'c(bBPxW&4#hn8+* 0CRwϵ2qC.|x== ;{Oc-u@sP :;ݐ $YESZ[xwߩ^Ftsf؛k_BM[g;VX5-%[z}u'jvk1GEM\3Gt|%$3:щw UM|SSW7r\0/n{:|31Dl[!Wڞ{}v^t+B)c*EW\{)-- %pIxŽʇx{mkٺtלּa"}B!yn3%~ ;4nHS6>@VFc*wT鉉%k1.6X[+uQ/M,7H@6>M0S^=1&HU_n5N,(W׽ XV3!gPp:~'#9aFQ>ԍBO:/ƁюYN*xe襗nxaa_6Pߠ!46~h͐g~4PʦԝztϞXj̮ ۽XiLa[#D#m{OQҞe?o:H9n)+*y4,!krH%] 9+Lcb0h-ZͪM6TQƺL~Cm$賶5kw^2(=p<^Y NhevkBTUM]]Ne{][)ܟo:oGK5Wvj"0[v I,aZ}Ѻs0ˤƾ.8C|E@w5qf??dN'K֖C leAD3 C w]6r%rv?ta%o~OBBx  @"@@2@ @*yW((@E1@ @)@@9; J*jsu M-m]=zFF>LLߵz4 ,w:@9z"  TD.2(rCGYoEq Bt_{}G7̬ -A'>RC /Ѡ{f> UEGC:OKh`T>z prġ:CQ_QA-բ.q>{?)Q8M ?T'jgOc>8>PC5o]'z81cc$v(5`vx dQrEkUI!*h'G!ur_;Úᓺq9r}vQџ?cpǵ'4YX=nPm'TPOkjO@"c'!jXq}sEe qbǙjPxׁk] F<'ZT?}:pЏPlj!Q"n??ڠ?!>IqKQG <q4AGcuAykGl>GC#OPuvx6#D;;mTٮb ?}jw&fps]cq;\q~k 8ܱch@i{>׉f+3@w1[}?\#g8m6qI՛b*ʵ78ǍdKHJǁd ]5)h- ͧآB·C>P12<}C^޻3<:Js^ӏPԀ섌Vs+23zg МQ9UlKC(zA@`*m b_==:>H%^0 J2dM {bOG'vQƯ6KИSĺa 0rnY57 񌒫"}_F`_~7F0F*laF0>sMR4(bQOC#BQ S&X"ΛB`TԭyӪ|`$6ޗ4D}\Gx_ 3{ 0pZ#$!n z64x go5ƞ-wwcPb&)m`VnV5Y# NHgOGD-Q# aQ:O(@AIih쯊ҫ֊F v% Y^9c[SM/vXpm1untрQ'4`Hgdo&j/0*|. hYж005O 猗!yLEbRv0SF^&/slܨk>U|6YQfct!*EYM."Fа 6&*n\DK-]f5jW`q`L$)3 4zУRI*dxic$7q䃩ndA.jf0 ; 5f@Sj`,#P6n fTԤ,} E;gXiO =F\A<҈Bڠ#cbPs <o͚*΀$)PKSEH)֑_f̐2ݼL rI32B^ub8xHԙ(024o2)PRJ}Ĉ/,c6!Xy5ȫΕ2.i%.܀[Y- a GeP=vL|9C|iRm1u֒uFDC1l#|'rp ` j5{Iss`D$QzLlI cm1#<@g%4YKbR ,GO;f Y͠G}TEa? .j.e}콫pZPĸ6I4EeRE>\*!%~Ѡ+#MJiuӛ>i.{F%x5Ւ nXM%q{Ӹ!+z9e!j9YK$Wi0cBz 'S'zN9H;mF!!V]Na܋c2# =_tBU] ˄[1)%֒q_?rFb,9K Ƌ 1Тkq y?3F(0w!}Ch38jjjMFVYJap_-F-NϚD;;TZ$EfuZ3#=~b9yŽ,ꁑ;މ0e@_ٹ 20~z6NΏrrV@Y M Hk/{"D:dK(Db_3P9j+M0I4:Pa@Zb@OtA =mN X{x'cteu}n&_302 z0X|2Nu]A%,w n:rፀAKl+nc$vYPaЗ'LC,%`ZaH[0"^![%x0vUZ)k m- /+WKvfJc)Z\xCDHJݑ2:pw=EBBt]Tpi̖qG.Ie'd! xU1 Y I KA;%ZVQc] u8ӦN_XFI +(PT]d8& %YhR_QXTNUu(+<#U״oYPFҲ:h]8}(:f$32Z=~rz48OGMn%{S;BrUxɖAU ) fp̫Ѱ>} C"fr#h0v[^E/ s8#TfKd{+bBpouDEF}~yN4*mSaXf8Q'(6Xn.sOQ]c`r"a% }F:Wo܌i"xG \hGB~Pz3XrVeŒO;}*uK@goE<щu~4,3s3Nٍ#V26d4!mSgvـķX ZhelT+X۸嬁Fe +C u~FnjV) 69eI=0Q1*Co]K.; JzPo GzyLZ fR0𕢒69HK n#=⣤gnt̨2:%P^&:{osjTg~9gpA`v~)Rf%尫c蛆TYm8Ǹ69HbBm  3nf 0W<Y+:z$Au)P`!F5[*g1#_P8Sfc "ّ屏1bA3nFRgܽFg ҒQ,R-ģ i0cuSHapyO"Ub22xFÁjPe KːĻG6'&*EzQ3H#GW< |$3 ZXEH!cXv'kP:cPK8'2bFϾHG-(ՙK6@hQuH>  eS$٫ iT ⫌(b>0F3d%ct i쪯:Fm30j>x MLoF֩a%`aP'|("y[T44Fq?R$kw<1-T|ثKGc+4v5{_0hNM?jW%ajBT/rk^K2x.LKeVlH|dٍ52v3CRj e .DǤ˹0[胎Ѱ'hv̐xX%"#]{)`Īr^1>$ي1tFq> Tp594cX*tL+h9*<#K,>$Yd>pICx[ ۞_03N% S/b(3ā500* 8E{rȹ,7 XaX4Q ^DtB NQ#:/`d1f FRŤGYq챬Ӆ&mW0e*[-Y%a%T^3C_&ۿrvY!=Uc=2X:~ٸί2soP@ 1,4a?疪☱|2yU\,23^md2G P%gBr.l츬xrm3[Joiô3 ``1cSZK%pV,0ȫk!8E] U ժ:!3yٜZZ<F,538fњ r$}nBpaD}5EF7Z鼗HC' v9 F}9 r^ Fav!yg! x}"D*' #NF DUsܗ!#0TVy3#m0 3$RR=juqpmBcp|lsXXgFbEH~-1 Ui¥n?2欵zNRKtxrFS0yonlRlSaD͚}UD˜-o4† e=2WgH-0H& B~̍fhׄigTu~Ibgh8>uSƟBI5l-o /F2di0 W0`*N8j:3h <#㾲CD%3:yĨX 7&g*208FrJeu"7-Mz#Vf-j`hЫTe&Q4AԿ+.aјM룊C B5CUyX5rnj{9fHê1 ziF͔m0t=FTpn{Im͡aN8_ W?u ^C/qȻ1D&I׻WXBBj:j{ʁԆ/$IZ#XGap6tj7oOk `I^sQE0 k{ȅ09/?3{0Wa 1Ȇe |ʸ ʾ$):`Ņ4~HD!xAɄ9,YduPj:bl[/2rQ Ì}5زx vPe"/J%ˉA (8ռB ,J,QM&!#<KXș=PF'Ɂ4S4H33bHԘћtHH.)3< ]=Lg1F OU\Px,5͸ZΨ~J"O70G9`P>SSxb؅, jTބ1C]`4pA1Xpu= +w#\\DUxZJY!a'o-0Ndi& y&4,lgZvjc%(p-LS6:Zcfaa]`U>Z}[G!CgTބ>Kk\ɑլ*_y,!Cox$kS`HJ'% xp/s2%ޑF)|]^3P5Z20v##V8Jbè0؎[&C*E#N]7i,<|>ബANVN!׵ѡ3# 25]gF:=o6mp7i- bH24n|X~6v°1L2Ù/}!;f*PM8aM0{e EL _dDS\Ճ.l= R\(UmX``hy$@ׁQƋ<6*Ng{]D֔'vRHHsM/b:a:R:;Ez3RF2̎ˢYU>EN>0*hPOjqR1M,;fȥjĎ*;#]6XJFK-)3Ĵ1113:cge # n}YuGWכш,!#>h ,1V3XiG~s(P.a@GhTNy0SfZbASIRE;ևHxd(X*;f8G.,7^:Fp1/pN̹9pJ+XgpܑJ24h9в|?l+Ǩ0r;_ʠk'L}[;*lc!$`ӱna_}ٶ{@xGrb}$ x[,8M]9|MX>æQz|Z+Cߜ2?+ N(˾b3N, ֪t`G!Q`2ka֜TQn1XSyfc/2aa}3+78F.F2i~mBkpDgdIx^3Ϳde#YqTUAMGobctб27%q08#fۭ# ]2, -jhm"'K2:ZafQG1'ϋAg f >[DgJʔy5IB) %F^Sf(#UR5˙aU!wcL0!#1(Zq2ayx!cX׋VD˃v㼽e`[C\ʗCx_!#YNc9],[,eh*WXQvi^\V;X̰1kɍp0-Yc2F6 ;רc PR?.f"Ac9뫼|?,rqdl#gnLҴG28" 'vd\Kuee,00B y3e[j^ ֙o6#sCUvYTVʨ!ɉu&7Q:e R2c(F2LNH (܆1e ÌCM#z .7v9CEc>r3McޭymŌ3v=Cg˴wo`OcDѯfh:Qjue#ơM"<3Y¸ .2(+9Z5B.)I=aXRd_햋^ }8jYU8E, 9~"zc {[.xo=U0R[/#D|)ږK5ˆ<l; Qedc$K+"HF-"$.  ѳ.w>Yxpՠsʌ~`-Yzɠ*CGf`1#Q!A(3G JŘQ#1 .`(ȲeH6۔g8ul$<_/Cf$}ˆN *bL(,TYJ\zhkqM\R_| /{R~y᫻1Xɮ/-4Ҷ0JNcݵ US:iqlLs1w%63ExnKod㒗xǔ4gЧ&#Fuƽܥ~ypDV^cమkLed5 KjCI+i0Jepdkg@'2*JDQɎĉg]zFetoY ?HC% MDOIAnpr F F.c{u$omuZEU ](yR5aE9픹jd`Tn jJ zF/ cA-YdP!.VA|m'ա#Ѿ}$j  *RԺBFQ[ljw2ޙQkLj,ARp=+" Leaw7{+,P<#]Y7 Ju:#f.N 3͋K"IedVtlX~UmLmjV7 AjC㑺a柳 (땋I"3CᲮb$?Ǝ4; 够Ia6֭";, ;[ wg QXzyƐeUv'n "F,"j[07WUMb:Sxi L\>1U@nNץ>0$w#1&EMq!:^"N7 36S'Mb~z4q ţ+ݺkّ\cB& \f:ya5]*'^*RtJ˃ݲجdbugb㮜O # lHheC1ʲ$7:)ŗ H~=gc0]kOy1_mߟ>ʎC7?#Q R*өLt3s Ff0ɛnLkx>G"f ]0ds$_Ou:}gq8LKhֲ^O 82ܬ&0)~qKь.=#;rdC"CLDZ$e8}xx[s!!N Z}Fv?Jbp J69ෝ}T~. I`jQ ш~E\ĥ0JMl%\=3z .b"!DJx% 7ݪ;ft*V0̤Xs3 'cpLY D!Q!AHdqFUD+# ]9v?ohXm )h'aI\K)p,GMdk :o i6۟Qmd4,d}0ٻȆI͞;]7s22` j0H uHam E-cRc\I$LmgAvKZXCU,37{4Z#h$ˋ ;I1ZlU}_1 =3%ڴ.P.A"U|#\gav ].prY#ۓ3^`Sm;0;FѦ;4\YsY110ggjݛL"lݝ!C\0x*NGEԦ["uW>8U -h2}Mo",2f1j9 Fc*[8mma`0cFf2TRMQ޾83Zbެ`$bW[0(3K\ e`-5N}bLtԙ6QIY^yϙk\X*W1Xe6"R5uqe*jFo󵽹$ 㘡m-d5ےc!R1FTz}r[:r2{C"+u<ׯqUfmA3Z}ڼ XD!K3Zl_y F17o\vǬc3K)a 71tm5I /1\R2=ű Q-upŲGNP'd`<)84I0浹7z3q8c1gjdBQğƜyݤ-&2ؿ =Gs0OiNs'{|?{?I?O"i׼?~owGͧ_{>e,>~>X3)s Kg_e³ Rr^I_z\/4'ysnʲ4ҷk'«fK/#R55\Z,m:-|_|b̯oi~Ⱥk=}El?je4gb|kR3oR5o#N/N>h;R»JJ>?Dn2=pfoWA/>wȣ1_|O^vq^O>zC>u>ϕĕ~L/ãDOrm.O|O=荙}CGk3o^^_[;Zv1|s3.VN"wK,kp ^߾I]9Ϲ/̧0?K4\q9s=ѹ(p' )̗Oҕ~{-Οñnӡo{fTNC1|}%lj twQ 2,_> /|}E%$sp)ѢȿbΎu*3{n?t2w`\sGdMgrX;yǨݠ6V~j_P>Cg|թ߄o|vgqv%?~T9: q%`o?{>r~G{7'Ti:Y<kG{H1 ?||hJ̹&鷘?=^O~su<۷ͻ_ӾyyK>QE}s߱x{ϿlsXv&=ÏEw σ۽ rOws3T ${ǘwO ]Ԭ~Ϸ/_[R/ݧ{{M_^?\7_\ 3)E%^v=}c|X3_״\\a{|qR/_w#ix,9[qg?; i2?Y:;1?O?ߊ.ҫ'>`~y 4~6 _gǦqz^sv%:EѹLЕ7+s$g |}zw8;Ύ-ECk?KoNߪ?cFBaƈH Ӻaot%u~"yZ2!D$Cی1Π{r5؏xOݸ6|F5v㉇G=%^G|O}\֏k7駮ܵ\3gyߝƯo#x!8;Ύ8;Ύ8;Ύx3(zүƖx?ܯl5◹n/̯M#>"~?#LcA&C{_?/>zǞҕkn|yl3laΥaʇپ$}}<;Ύ8;Ύ8;Ύ8;Ύophr0$Th]|dv@i)m} V NP epcrom0Oh+'0T hp  PowerPoint PresentationoweoweSumit Gulwanise1078 GuMicrosoft PowerPointon@PN@@p$)0GSg  )'    """)))UUUMMMBBB999|PP3f333f3333f3ffffff3f̙3ff333f333333333f33333333f33f3ff3f3f3f3333f33̙33333f333333f3333f3ffffff3f33ff3f3f3f3fff3ffffffffff3ffff̙fff3fffff3fff333f3f3ff3ff33f̙̙3̙ff̙̙̙3f̙3f333f3333f3ffffff3f̙3f3f3f333f3333f3ffffff3f̙3f3ffffffffff!___wwwf4'A x(xKʦ """)))UUUMMMBBB999|PP3f3333f333ff3fffff3f3f̙f3333f3333333333f3333333f3f33ff3f3f3f3333f3333333f3̙33333f333ff3ffffff3f33f3ff3f3f3ffff3fffffffff3fffffff3f̙ffff3ff333f3ff33fff33f3ff̙3f3f3333f333ff3fffff̙̙3̙f̙̙̙3f̙3f3f3333f333ff3fffff3f3f̙3ffffffffff!___wwwnnnmnmnؙnrݒmmnüޒⓑJlCmCDmnmnnnmn⼼mnm⽻mrrݒmnmmnnün“nn⒒mnnmnmnnnⒻlnnⒼݓnsmDnⶼsmmümm“nnn⒒n՜.+,0<    On-screen Shown-sK{ Times New RomanComic Sans MScmsy10ArialSymbolDefault DesignMicrosoft Word Picture4Global Value Numbering using Random InterpretationGlobal Value NumberingOutlineSlide 43Review: Randomized Algorithm for Linear Arithmetic"Review: The Affine Join OperationSlide 7Uninterpreted Functions(Nave) Linear Interpretationk-linear InterpretationsThe Random Interpreter ROutline! Completeness and soundness of RThe Abstract Interpreter ACompleteness TheoremSoundness TheoremOutline"Loops and Fixed Point Computation Related WorkConclusion and Future Work  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles%_+ Sumit GulwaniSumit Gulwani  "#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqstuvwxyz{|}~Root EntrydO)Pictures@Current UserSummaryInformation(rTPowerPoint Document(!ODocumentSummaryInformation8