ࡱ> ,%&'()*+`!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˽z`[@LȱqDt(x}#.#.>>>|~?>?@?||?||~~>?>|||?||~||>?|x|x||>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>@>>~ n{HeĖ8PNG  IHDRM<l pHYs/tEXtSoftwareAFPL Ghostscript 8.00< IDATxM0 `2GQ8,YTL=ߤ.-jr+h_ixipӶݴ*7/t(K{BKжVUcGR T *uRi[Bk/Jh$XP ( K`i+//%`NYJNe*oRTK,XOzgm|9oFU m:ߍs\h UFVDt[Ե&n\ܜ vO I-tQTMFGu** ZD^8}L2`E^8]uDj[b62$ BQ;t%8oߔcn2*LM_z\Tm:9 zUc4KJzNҘ,?M]m2=o:X4jhS+O?ODhQ{!d LD^gKдVa"yG%(쭑){kD5IsȃL4JZ#ϔ53%tZ{i>-_PG`}A)}sI`픵T N:uzQGq;i>Xoi4zUN=*`SOʩ'Xмܩ#-T%TANştO?$ו!IENDB`nRDor#&PoSPNG  IHDRKKgAMA|Q pHYs.#.#x?vIDAThO6pF,=@%_H=J/h#*f "[e6g $y';caTw!NQON)S@<|sa((JՍ zR  /*Lk:Ŗ(u@ mTÂ7/~J?:K(ٗL!JB*=:s4Y0*M [R4#nPՌ Qcq8]QG7UJM6f21ne51?Ew6]Hb6Uz)K5Q0UΦ?5)snm=63Ua*QS$V%Oǫ")aS*}=`JvKǁUԂdyA5U0MN j*(v3XT>10UaHv'kUu @= Qp \4}R"W[Ԛ2"t J(wUQDA1;HQ He!GRP$\ E5EVItE+JȘ r8yvd5%QHB'hjP^Db@(7P'J,iLl(`&JU-="ͰrOd(]!NeTbV)tmb$SUfKg%2j`-D]'ʝ(JU׉B7z.":,[wʼnATENzF d= ϩ B eձwCc#]~V mN{/vP8Z-ϡ6 䣨C(fR{8JZP=*b%%gރ-QP̻c(jluO0moZA MRis%RT5MA‰PSR)2'6J|qj75gEu((/rF}0s0&NŒ)xZ;(=Wg}J&JGY!ϷR՘V0~ALP`|T|7SʁO1{Rn>BSKgZi5hjr?E:)AQ.RUL/PK>NX,KCg s(Rwu"~ji1s#:>l 5<_rH-{e .-oV궝6Rs$uTZXs{񸅩%/VjK2b =~KfING'FR";8m|/C58 agΑIiF~|6yRN?!? QŌGSvT.mF_ Dm09q)M*aZR U}}EmESv+3Q.~ҦZ!ewnvۦ%++P1 U1mk6ٔ*PBhĈ !M  #>&_EP!iH9s]J[$'9sfΙ3w-8e:/~]>X@hHnlp'Hhn7#ߎdw _ &Rn{߮|6'][J>;e T` дE#8v]࿓bT*[ Ԅ[ USct {nj"c]XnTJh:݊t?Rg!~Y#8i|.Fe^8.olί笚}+6v'Uf:-<1d1xs']f;z},G͞oN_Ulj~ 9mAq~ <+sYR~wh7}΍n{uŐmMwMeq>[`֐i`|Yݖ']**-G|4'"-WZ5/HHHopgU-iI<~ C<}D6CٿjBFޖrx~:gVx;DD6ڷ<yץ4(7zrm.&ܦ=#p^3poG襠- 7rugϳ%WGԋ2o izom^C<ՏSb$$vMJ?K 3b˭3BGvpnjXDt !\d{HG酕ɉK+*{-G~_ySHA^} w ]3зQaJ~[H3?hOl%,%ds#YO8|H騯-9nnrlEc J'J܏]͸umln[gֱvu!nz.| Nx zɹOu^s9Y{犪]Aߛz9˱yO*QvcvծK'VKθ?u9+_a=$cShь [W |'x]T+Uj)eڿH&+UKO"˶Ӷ.[ S29lwF`,-c}uG!ƻcG'ДsK7~Gh m{'@=gw@kP}|l\uxY]h\E>o~ ]i[ö4?bHE$۴H MQ"k[D^SE|*O-P([7E""ߙ{f5M80w9sf!iPFh%Naq":KTD79DYJ"*KS*XO71*Bg99~Pa; 3y,'o7$ '!3y,G/'פ,G5Z_uiI]{釉}kr^W18@\,)xϾߎ>} վ mڄ#_.\罪Kd.CJnwCt5}No!`8~3M:pNg[O;\o?_oS[*DB[~SV?䍲TlO%b~-ҳ1 }:LZ&eBb= `0uڭ0mn۝w7ո[:Xq/n)iZn rUd2 X%1^_ۃ<}؜cl_<^8H`ĝ93Ϭ31g"n(JR{vyDYv'$Bk}\}˙W| V{쥶-ƞ@D{t_K=e4, vclI=q{!hq۠ZŠ#ؑEhlv9,?y s\6|al_1Iڗ7;g}Qsr\ut_gy{Y7{8`_TETo(@ |  (vPicture Word.Picture.80,Microsoft Word Picture Chart Excel.Chart.80*Microsoft Excel Chart Chart Excel.Chart.80*Microsoft Excel Chart Chart Excel.Chart.80*Microsoft Excel Chart/ 0IDTimes New Romanll 0DComic Sans MSnll 0BgggLP ;oComic Sans MSRegularVersion 2.20Comic Sans MSBSGPJ`|:cW h1:9_)@gRNP'f\g6;4@ezd]g+NoФ ;P`}qIA;]֪q )[QMaCkb. PUn W$q@g am~)zӄz`K-}6{'a޳ .P{SySHYΐň1:Ő6Pu ͜κDvTppV!RX0糺Iϣebu$ td.i&(:DL|9ESqhR!h RM0L0d>!hFd\tOa01"idqY+x=-4x{Wr.>A@`]d{NJ }{i~` |@GHbUN} }aJ!f.)=Iong,Ipw8 z=GRidSlÑ} Y~Zh?~-h^dnc:9Wd%}KE@)Ƿ>~%}X\RBMct d:84G8rC:њ㫷!v+UU"NTW~HFPD.Onxs^\Ʊ(p~dm!,3:%,)PJ3,)fyV{jzH6J1Ŷ_Aeu !կ >*fbMJ p>lxE.\+p+Fp GXóN0^&c$Z3!C~Q + ?s~4ltYױTd*sILi}`0e0?03"uQFE(ԸmyӔWϛ 9Bxj _J뵄-UڏT\s0*ႂ$U! $`_ 52<@GXʗu[hO2R7\vw*VN({˾HM,ɖwDiğ17l F`V)YXbImV(d IS VPYB "6sK3CgUQ^W[8mY`!LIKX΋ $+P4ʃZ8jOSzG(ҁsUs4Ӎ,Orr-ſZ.FJPjpJc$~f3|H$fB`'@$8D] ;EOwI)Z_)A/f!6Z`J; Ԝ"+IH'pP{hJW~p~e:2+2Y=qA=zD&yվg/ '@Uhkqȫ;Uq韂j8F|y^49:! L04oK-HUK/٥6C*^H<<P#LcM ã$ p,@ Хd~e{eh<D% Wơ$ƈD&VE0 @mfn=^ _@^5Q{^ NcM$çh/D}V-@mP5)pߵ[ew;IV໖)"z=4(emvy%OV5RM!ͩ&gwpۮ]eG/NYNr7 jZ#M(;i_kuCqTA~.1jM#CQi4jKwb`jṗ- 9}lq)@1{[ʆZFzq4L^<Pl8֢S*Y̔a ԭNb\I|gPЇ\%)Z7xJE0@s{݇k2E@;HRKba@RO@ l-CRtxO`;Z׋<=aw̌|jkx"C3ۇ3C(>us^a&k$F_mREځѻ>/d%7bԋ򸶐KwH+ADa 7TjPA /*E\ZlAm;x$[3%d@q]J9dC((us,W6 Qb 2y@ɎbKI:)+Nm"{$'~A?vnFy kt29t"`%G2c4vPPk 7i벳*29wWS5CaZs$q nی7c(֪~V)^4U ]QGA8f(/Ej@SU e 1'0"Q@ ňAJ&[UEy] ]R)?V@RlN8hQcF9@J2>d kihwA_J<-U ]p9KʓH0:E1lN mP 2+ᯀJ0ӬV\h'.DI5H\%@IL'Poz[*aR1-/(LdGnNB5`غ@5>;pN[ޣ[-l0֛dS9QP#ێ 89* 3T\4##A1*R jAgq;ZƔ .ԓgk.]8kk&pt (!-5>MƉ^,l[FQi h?; A>xP ;f.@ub䤊[5mȘaʈPJC!v'룸r~O9Zbj^uA0CD5ӒM!"8OFam)P"0· N_u^`%0ab[Q~Kxژі3zҠ.-PARC#-8}8FA5uLho VV!AFͰPr;Sb6dA=E P6 t.fn '&i;Iܙ3;E6Ky}4Gz#o'4ۤ*Vc`v$6cE}5";){F 21b Tp(鷣ͮp"VTkm-̀ԓMIhx>G-[bGE(iYtjϐ2qbZq.Pܱ]|"^"琘= 5MV9Ebk"ڞ`MQ-Tlf#P3N%uaPGX5ٶ f]]yta0j|ɻW"&ÑZވ ZI؊%mD'~ېyGRDta4 ܤSP`8B5NLixXvω%&!'gbuh"P0w +d2uq[5*nIndaS=gθdڵ/iVB(5Zfe4,:OW&MQjl0Tl\ݣ,5]U F\Qud< xZJƽpYb%D9jZi ip:#8D@E^HH2Tz& I " /)hc=8? A V-@ R' ^鹎/Cm0 kխ/iA `7HZ_˗#7@tCg pBkdDm@~K iN&9E pI#~qbCy*L,D5|+i;jwdu,PMF[D+%)z3h"oK]\*)ZnJS! ujD"Y\eKMD+> RH/۬dR|igk<.dJ Dx"(f< cFƦ=IuJVoVRZ=ĈqXsQ3"FDel$.j!َyt;/pG @(5sHP)jkup> 3 [nE<"5p^S:pF1UXgK*B v>&FͶ0rZr6 w 6qU,}K4KG6M ̄jf֠1ig.Yċ+c k?NC8@A_D>TZ0a`+In׶ع$v }A5 (PY(Dl A"WtB1XTW |"0l@A&P҉aW]~JHBx2o:0f[O6D [B;d` M_I*XDIo12kD / ?:N3K`Z0~6Fb iDD@$"4xAx:A!!z.I31]رr J2K\+z8&`كn4`R%@'֍<-*` 7i }r9%X"$P*H~i0끔_I4J@L")x1* ׁDJv}UiNאMJ@VvSEÚ,E: %_-UL3t<(ky_eT\D7CŶ5zHbV\-s(R!Zh,AxٰA$%E3 ;PXÊ-`,]kQ7z(%帲Rg岔Ľ>2&GX$=tRa^1H`5db&M%¸A(z8e(V }g|e R %Ӳ^PK-ҟ;8 z)"I< (uq(Ri>* @:= vx##\2 ӺVж}/ Ib: N<)/= {iBk])z2<]60[k?ia(QܺN*(eK_\M Z:)e%$ O7a Rg2aF ~}ѻ nŚx:H!K%J9C, zAW̦EAP `L +R !K22lՠMY-IWi̼x3WH3z7Gp/xc˹@ WhbBUY16: zQGW/Q1]XCaNj1#*E7 f :4 ]f=Sv*%B+d IQ"3}x&@yO=p4y9OGUzdE:]MDaep>? gH'vNm9:J}5pshivÏ[EVu!9$/ xgWZGdΌA{ٚ1`G ]eGgji>j+ WxaM{stky2ø6{ژҌB <"-RWh:*I&OlC(EqT>WvtY*t8<3O_:lPwȓ-8D]yxr:_z〴mr1a,l  7CDȦ#'n5OxN !E<ʑU-y dN_ ( +8%Vһp3˵ʽjGUɭ5/~ ' B-VZzx{p{&_mR}0`g*&ru-*#rzd!G hhp=U9ERu d(CD@N p5||S'b9MFs.n_C[9_KMӁd$ڤP'[4H&]0$Ǻ<l^JF4koǟoأ{4RioG)bJ i _'!NT`jH:N-<'gDi͔J)};k|GFcb?:/]._s~zq>Oc ҁd)%e%@ȘFAVJjJ$U`s!tc=elB rS*S p{ xF3A%byS…Hmy܌ÁQrh˨0T8 e|;*MS1dBthM5I8`rH}=P)Ajv wp8=De evv݆+gZALQPa ̍ (BVĎHxoůZ,(`G{shM|=~r ԇXG_RRLSuX7y( !w ~08:0]h݁<%T@1-2AG*^~wl@%`DAYPhN;'RysC_Щ,#Wr<O"}n/Gvz&ΉJ= &P'ԒL /6*plke.&V8Z:?D8`{L99jjV[2Vrۄ_#e-RBj]@raƯq)Y# B5眎Μxe-ը/]}Whx8tNS i/+ +[ȁI1ÝBM |XxEpB4d6IϷ3W+̄'}v=eZx38/HYFM? @#N?q"6x$M9F\zE82: C,< {%ݟqwdhG(7={=Ėac8S8J,PI1w4v%l[xX𜸌<aVLJ5Ү0T$t`RjrXL9\E)Ę'eCɺ|iD SVU{D{[bTZ_5 !go?f냔[u9pd``OݐwlK0dTe*ʥ=[]v9PX.2sSU>ǥYzG %1 z 'Wd?$b93HK'L0t$n58`c{SlGfq.DKSkh L $%L.zR8`_]O'R:aaFwxna o H&o>zGzc;لe<˗ՀȢ"7{a8/"*5+ &vapcH+Yw:3rT|<4$mPpdER:J<J`]_ 6=CZ=Rñw ^L5% B\lĆI @?>[\;«u8l[)̜zd^עC H#w?!2ڎcK B E/r}1.`NٔS0q 0%H V%!{1My5:PM>] خ~ͮ]CWb67hs)T"ؕ06U0<Hy.C"{&wXYdMWAp_t0ж+$1XRRv=~c,fx'xPA17hl.G5K̍Z]PjLV/]r߰A!4[ie0\?66◌|"P2 92,yJhˇ6Q<.J^0JP/W%d`0ER74 zߊ=epG3Xu<-.C`6]nא# N"DrLWof-}0" HXK)(niup9fQ U?"bܹq⛴s<9 [2zmi񐢑 G2p1;vSH 4L&t>򓨍!SHOΧsG -k,<Хr؈/sLRWPG*meLdD!7R"+J4제É%/ {L#h"cY2R}dΐ8DQERR%:';+j8zCmqAyXؔ- ib[ ZXcr1M0is k@`bQb텂w-usY992dF/ND8<n!TTW* 'mǜW9î2kxj`$'@Ӂ;$7o(4fl\{|}q5ߚ~+)6l՝i xr"y1?4ご"S{{/.v4n@<1,*F^UO_:,Ɓ~ NW=Éy18E->ʂzwq*&Lb =}TM Y cufg/-(%Hh!T_޹!k '>N6CPQ2 )bR4\6֎ ]H 3v-)! ]zWhOI%ϲ-l;YRT}}?)GFd-GFy@S):Kﯶ8/Gse< us FiՕb.GNJ}3pRhp z(\j`Օ [ j Бg>nʐlf,eFAuA6^Va+|NK;-H+QBʊj ȿ1MT6ZpOwaJm::G~5b%.,Fɷ49 kSMQ_&?Epa5Ic׾b4 :! 25`֙~ =bLmhy?J3a.$h FT^ g»|Od3:~T|/u$}' i'r_^CD^Df99c"9}pd|an!uN^UT O ]3nZlYqhn@^3MXʐDBW1 b P*DV?jDE sWzbG$mTeT3*)MׄXxOz薌8x!SnM)y_['Z!$GpO\"y8ldzU[c7%[:d7JwQBc@BT A.g(Ƚs YED;&FC~*~DjL0)a@LuIDesCnzLiNJ.,$cKZK3Դ&< [C4U0YCFNR Ph {X#:]ʳЊ# ݛykGNRf$俣YnȔ`X),R$aIj5\nqN*P\ jLzP&xϗjDnC[X t]t*EEIczIJ!% }hW /5v,wy:p-n+d=ax ou$!$;pA$"GT]}AjFwtE2=^nXquK8fǍZZ e22g#Bw@/ MR!aN )s`?׈\y< څ`2l_+^}lqd=5onڶnD=-ĩa>CA OIbZt0[Joe }=9}Ew" ?`Kh*F[ݐKS, B^ R_h`q&a{(Յ 0,*6NqN 3Ƅ ᡮ{w'+}eWUt.i+@rffxtFjx]lyo:X@&UQsno^VGq,X0IAlv5fHp麐EMO iZloAOjkn;!RLiր6b2Hg1"1`c3DT,6Ƅ.u5F7趎SoB6FH)B[$| gne:E_HLXC"g+'@rhx-JyZ=K ],%rMjjyZVԩV|nj;W`6qqgz*z6ݱ7dPh#99443,(AEv˳hJ3Ś")h?5 v,ObڝŎXԀWr\ԡ↬P#0(ivj$AZw^: rCTTP2yn $5J 64 ЦCW4(;!gpAPt#J[Ao@[/s!RIvOgeGs0P1R ZA{ Sc-iEDϽbkWQA06 =`Haz2ܨ2Iɾt_`=$Z}L煌SU:DI텑Ge2G_gUjҚO{?yOKGG_37&ٚC''(hT=.k/0DNjH %"DR%KAn`mPd. 4CRt&;T}طIQH]Fpc"%OV#<]c;7k(s+Ia^Ȫ@R1BfzB `f-)هOBF6z f,h+a(’ڡ,pG(_X5iIa]je+&߻?2`%Rs/5>y<;lz2cx]RMmf#jW$D4>Ĭ~~?eTD0A0*wC>HEV ]o>uRKk* !t1" {f- 7%Vr?h14)Fd z Œ`3J$,vZHTpJi`HY(k\ %#S*BIHÇěnxI"Z* 7MBGr[8Uj<4|aЋߧH/(5ÒEdL6^1N|]beV)oV.jͦԝ\@QP_:ü0Z,LPt(h"ϩlX=^!6q>b|.G xc)+Dr{^(S5"/țI.#g ף Vñ-A1yrcZKjCqȶԅ//|Gt0\K{":GD]Lh'X3MҙzF)NS"1'ĩzT:^EU(*#*<}ut^{Yc]X >-4 XxG 'lR2֍?)M)< 37tD(ŒSuF~1Bb+b`M,BKRʶ1رz0#@0fPPs`%c1 !ker WLR8kJܴ#;j|l:H&A >%09L50kHDaaLX^ٌ 8^RC&ܾ2r,8ʒItPh"{*C:`å TVK9ٔ^6HI{.0quI}\y r.tT6a,o3MZ%8ɸDv'))4D@F4#៖I"E -tӸWEJͣeEPna]O Bp\wvR^p!^# ~O#Z, ִde4׉ʐ3>㫬'+ Q֔3wEld|4/3lvWqMr!ėj$cq焭IƩ뎒4ݨ9de;uR穐Zr7zDqteIhqGh&?tHu"[PUbHfH0  B@C4*<&I%*=ml)PO|VVϡ\5+S~@Z u' ûK$N]mhW5AkuFtB˚"azfiR7%,) xK&~aOW!_ʺ"v/,M$֛eUZ2/n ڕDa[-̈mݢϿ)ta;&@' 1=6А\c1)ŇrZ3%ѓ2@w6j1LShؼсE4d}P처$Q?=ӱVR gx$#$;b㠞Kɦ`|MuF8Kj}M S;uG]^m,f֮aRʉG$\` ƷwSĮvR ,F{mn0 p ZDUa0$Ut>l7/|3tG駷?@GowU>kyh $㴜'\@evފ77WQ\fcl. yݏ7* 8f!ݏcOS[}tqKyr}VY[{ЪxRHTqs98z[倐 '(ؔweGi8RfI5P9!:nfP픰4xmrxvʑXw^ԚkK] yzN7qgf*7jjԯTӻVE;`Ib}/  DΐcSIޤ)jdI gP_.-P 6w (Er|o9}BH Ae"Fwlj*t6}vt|?>wp]xRd< CߤHr5Bǰtys *9Iw $D 6 '(P7I<{2R?X/IZ9:PT;1F5nO r EzdF{:=x]J.%#WJР$bI0w[bB }sC]^x0@PX0^Jm=eQUY?*S=ϯQcWMQ5TbNVzY^7𢕞o0xzuVKoA9 D+Ƨ#PZuA@wttånqޚiSz*UˏWTga&̀ )>;79d_Gψ]hFhQ3xpaWB1qklvYřv ~~~rɐ-^ }z1\:X^Bxjc1,{ Db,Bf Rﻳ Q>wx[x[%?GTXY28%ECic2ǪzYSobr溨䵩N"a~xèLAn"<30f/DpAYgw稏Q\.,=+q>o00m Y(YҬԦ;ȳҒ4ː#i;9> `Sɥ,%y6­U>9`ˑ`?=T  i48FUʔ 4-=:<`s8#-3`$Еd'C!QЅC3 @JP`2Hv;0#wJCWCHۖM 3W\l\ڰ>v@vШ⠕hL74"h! CAJBB!  p`3p~(+A0U` P`\_Zy8 {^]r^,Xzzi,6`aAj9WϜ @\ѣtq b9h u 'L.O-. \)ՊTK. 1{K´ݖڮCVkK\ղZ*Y2Zn?DȸuTgʦ>ЖRHa?G|1 xϺh^;cJqЬ 6!J dv8M1s3.wOs**rWp/}(3ے.,gXҎp '[KE)®8!*v|tT\k猖-Laa`6$4#j"sgEà v` FHjEߝ1NEAa+-i@QQ+Z)m 0"f3Ddpƍ"h*a,9%bҦxV`+ ,i6* ]er"qؾ#ZډL͒Gi`7enk.eyT@E :ض~j הF mqC_؇6! |K{@!) )g4G3#~(+7٭Wh<-K$@j$҈90v{SGf&ʮ_L%i8P8oP tiJF7Aj(jc%O:`XP6,O>B {ri j!o˟0Bx$v*iN#C=b@ PٵO4*)d}2F4\u:+ ҘӾvvЄ%kU-`*(iq1?k >5=7ء֛2ad ?VQoqy-1OD B`rIs+K쨣s%*a1!f@# s 7&ʑq=f)!@3JzFJD[X%)nڡ + y@tVŒXsu@1 Ξ!vɄID~. <7)zy!88PF87[i F猜c3JWŨR Solsu{r@Ex.iAh9Y_[(3m_Aξr[y; BB n~:z> QڱYe /'Ǝ sL Ekb7l歛.Qnk@BϺwE _7a]7J5MO@#xGwAFb뀃m}6#'j4ɶ~n*Ά3݋FZ@7F3SNK.\YM^! e3bމ}Q' K0vYu^<`|",a'!+SYݶbMVUƕ8 ,@C)5(W"\RH枂Kv ]|9<}?HiQ)˖q2$MNK̴ڰ,wSfp*dBDج' wNh`Q;;j|ELDwu/$PIbt _C)LH+͌3.vW"A07vd2 Ӧqp$ю٫YNCR^5kʒ$!YCz-; /(.*CU3n|bdn CaUMw!Ik֣ 78-&ȂȂ"#80>[?:eK?v3$1-@P#Z}؊yT<@JHe3(0ŝe" x|BܾZ3}74@EP8sdЯw@"0XE\0a #@I*ئHN-M>R\.Os>Xlg TXE-@Y\ z˙+#^†Ќv|Dh>@0%r@rG h-4SHѧr Pm+øF+'uZaDM,Ml|v.! y"o`9HywCm$$uԾn*wz<.Hj7-Y'q{(\oC4 IIOJx(Qw x`G- CAd\->Ԥ:'zM|] rVW_aH[Juog>bq3 SLս`F\X`2Z 6G^C)ߕk2E<' rYYPb=T޳pkm#f' AB!/ʝŢF`L&{gP\ ewȭAH79ml*é% w+,yCB#~?35(KvEU$hʲgط9P?ߏ? 8B AD^:oCuI{QĮM0$ZPX ^hc]D fQj#/ yl"= 1!!LP@9ۑ F΢˻M!+rjXml[KWI! .PQi]T >!={e_L<΄Rr#+IOqܺMjYC`bdx_}V$+$`q\^קkw7RLq S-e# kV.[qP!R<|$82ryZQ1ww~aDs%;p8R ;l$T:PyP$`d i-OȜɴ+>be9D:*bP]V~5]WȤT:߬_2:vHE  ?"&zХ(|Bɹζ(q6f3_M5,90o md21zHV)u~]y,K̏n=/_񈓁95;e8jA? qo`( qxdeد1g~Mu1Y[i8b-Nb.?~EPDoa#D]3^3+0Q \wb%cBίe@0cȂd3GE/ؼ+ =2p1ek")ch9 !A^fb[-YliDH&; 3uy ~/9f,@"NPߘNm O5ڥL<M.>XYb^)PBxD+嚍ف6Hb@i4 dnW;q% SfS `.6g MP=79O@sb9U (UmPܯRen~Y2(!C9w1lƹ((D"A:GQlM(f u310~xϒ0/DlV\XQ^e+`oTHzoőjn(@s ò6C,~ٌAZ { y ɱSI;v@apγ14f;-^-N n #jX/SIdu,2 4lk͘/1O[C؜ɢdnM*NC XN{?SҎǎpH@9#k4LjfXj Ua #!)̻Q@TYxRą >PDY]q3"6e0S0(ԣB6 7l6VP\ڶ g2vx] X'NzK!"h͕(hf % Qc#b ^PQHc _#-7[pA150P+mbE FڊNI%R[%ztF% dAW1 1&u 6JBXĞePUvmbXMAm].]b:љ3}ǺAO~k78 (Xԑcb2u]u8n,dx$$\ ىdRb&Oy6ܣzԩ~Tl福 c"w;@)Z 04L U#C!$!H| @V]=1E:d2 (פXA;V 3v k=?eRXب/KUiRe:u\[=V:Ǣ26 TAQ8#vrT<6ɂcQI4@jܘ9 @Nɠ>0 &c,Ɠ5W4fCQs]ǏH [Y+I(EdwyUUT LP U´Comic Sans MS BoldVersion 2.10$Comic Sans MS BoldBSGPۨAaO5cW h1:9?~A6z&e} )05"SpyԮir<0* "K#%q`7>m43f5*h M"KVo9X`tXN-E :am=7lICFɿ 7οHdn˥K9x0^t{*DFk;knƒ4m2G *db.Y1-(!%f1?[Y=߬pgCm$@/daѭ]T_vpia5tA)w\[T2),B:g Y% 5cf=^5sWK̀!\焠 쓢֥M<#RJ$T31ǻ@H&{>6;f~*l!7b N\Ցk:M5%Jd*o p!$,ZHKmT}# U+Y?f-|=tuIFla Dͯ`0IZps:kd(&G^04VcZ橛]iU@i1nfdV$tahb=R(ۇFҫWM2{8iGQ U$_]|+Z鰱=-rтM !8 ,s0v m d[OlxVùX$K-BL۱s*=x!>Ev\Qu#(TK'<@ ?{?O`D(X>HlZX:=b^[Z-^L9Oh13Wi%i6UuS)3 = \4 $3S)&p3$ Q7Dwr4,N{֍{7֚\%>Z%=a~ χ4z+rͲ%xR"xK\,\)!l4Bʔb)+h=f(Sf6?OkIFQ_Hq ˟o ӢU~Dܞ Fo1zJgоDihcXEԯz4`H~D3T(JbܨH'+`k4J'C ›M#i+p Jð; Ga" DpdAU 0i B8I Ա If$rd%\ |Cc@7J,^*ۄ΄4]tƞ(|G޷{BE*aip #$v7.&)Bg'Xʼ9S)Oh_},<RGoFPQ](?+nUUވg-NI0"\δRVyc7/QML<&T~q!0#p}A@ϑvRDNz evDY" (|OkQm-N^U&ABf"FJTĖXzl |Dt60_6%]sutbW-<-A p3^g`ҴDlKDr`-I8f *] - r „"y6P*}\7*dc ?sIzy7UǖfMcq,DyO7YyT!υF׹Rlq%Ι@D8gv6dqƃز@=ĥ\D,l2 R4\ujzPRew i/`S1ϦU8qMd8y+[5l [R  UJ_@n* Yz Dw>x{Ey Q)Ίi抓/ * Cral "?IԼqHjT4Bmb9!I h$VD5Ly9˙01JQ EgGpMOd8䐆֙S6Q_PHE8?.1ՉTu}AP _g+К36XWn6yrĩ~Tif/rS#,w6dWn3 |ZPӧybt=rx΃`D,JgI$MO S* ߵU[Ό.\ƧD*lE; V}{2 'TSSCjJb3ix01I¼!yHhO B'T7mVӔQqy aAUpǃh<;mM)w?,A(,=tf翃V۬ P^J? e:H6=YP$ "ble "EZ#jZ׈nC+ّѦBĐ ]6>Zb1^RN G,ut50ǰ`q28pnTID fR=qCzZ8HkϦ d-6(ʿj[M5E7e#NKr:[,I7 !p%0m;> j3(c)Tn!880jgֲ}1uM44Tc6/*r^wx]ti|SBz@8K1Fd-~ ɬPL>7zxx:hZl?%E9Ӧ@SSnRa;ij'=8pmvf?'l-U!V_|]'%aFW3Jޱ]E_ pr+?BJZ-VDJ14lb O<⡥G,2DPd$n. VS?iDGl3w /w[$)!ΨgLܪW~]d4XmCDȀPɍ#CE :B& Va%g)9~?Cd;wbW?WRmꄔJ ?UV06~E pK3UP:Sn(@'B!%> ԇ.5t=."'0O[,ccuC:[~'*~sak*5I "I[C xm8 e6LeVNiv-D{vckUjvfk1%g.%Q 9Y2,m%lt[>j":`R73}βuMZ'Z#˲-U"Ș?n*A4wҋrF |(i\ ׬-7yVe5$@ 5 Bc(F.K%E}&n#B ʑLN#:.;\ O=>[yēa ysl|1 PoXayUڊ]ӬÀ2{?yIgz*C+W1QBnlkՔ4`:M %!>5ninl7vt 2pnK̈L Li\-8M;be$ mAjC}jA&ѱk3Hн +KoSO^&B-+Sm` }ז_`Q0?blن83C_"GPD =a M#82*1`vX4b !A"1ELb4g;|)DJ$'ܙӔU+%[!ț7"JnՅg0up {cѮ;zpω%e5 O1B=9? yȜ/+kkz@|DA6#'iH5ǝr7Gtԍ9)>š'%P +Kh(1 k-nYPoADh6lMk[.SMc =~%tt"A ] QLZJb{zxy{MWDպ!`jKb_0!lhT)tpC}OkSX-i@콺D:ӕ٪% !J 9V_A QP͊}:m-zIoKa1>ybs0Я)3i,Wh[bdO,v, G̓XAqƋ,Z@lyrO Y ut~4hx<~c&%fh&u_4b=4\wVB[UBg?AJgs7Z̴_[sf1f3&1FdNJу[Qb?ic\}܇?`Qy`fۋ!iHYBp9  eB#Fr{1F+}Lf#|x@W:4v`3*T:yⴜÕ̒y)KsO0`!DuDCPRny RuFZ i}i.p NJ 94a Zt]Y;Y,?7ii1/#"gmwnWİ媕s.LvWx."!`M&=T K^UmDTȠsr*9vՃ䤘O-iACЙidVƥsSdp^ZopP,8%tj[P.eMeHq"bmd8c^z㨫E=KWoP`a[6n$3UD?8цP YL 'ghpt.0T~[Zv TGX\M~p'! ZgZ| P>|} ecN5nQ(ȄɉƦRe:[ xhI-yI=yG>пM @THՆBIf2CBxYrAH+ p,]6T]7iˉT t֐6W* Ѝvb]r^FZw7u3 (Y܄:cwa[- E[2ev8908Ii^&u{f .2HlqY. " n$Uw>mPp `M${}"9=Ul:~n5W?50S-6%g6K,\L؇I8x׽. GS3n-بE%tMe)ʀr=EIŏi NٲP#ȅuy-a]VT. gMhv=M([OtV ;c/Y5݂R:IiWVjEL.0bDidbkL !I%ר94zΞ]Z1m;40v4 AMah԰0Oݎ%֖R"0yKMT8EM 9b4C9'f+9?h9X^$%@8TS\N>0Ъl{.t,X0KO`*~Hdc1!xNCsC|vR ‹ؤr:5~vGhHŭaa#m o SEFyzf:HCL&K~@@V숅+\!~ْFi8lGBH,{0bC1J̹6(P؊eyx0'a Mbڂh`k8}?)zc@Z"YBflp" l3+~OiXL#ղN%!{kQi_%wӳdmRFJ&+~`q>Lp4PԴ!qICO5nL7eCk_ 0EU*(6ȕ B]1QIܠ7$;6r_~,r@&Gk2^=0lt4 R!t0HWIy ^!+XN<0(&$jUvҤ"ő+'$aިHSOHATН =X> 44F#SSǷ͠φ2hmt #vY>!`cFOj9gIcմSpTʨE!hSHW߂Nrrc5V$+ #6OZ_Kd(.Ie7I!t'=}uB8ʹOL Оz"MlcInI1.{8!ѡ7G{6SW@N;7/n WWi8,ƣL/n-n#0O-_ҚH%ZTbP + ^-UbB)鰐L u>o4< AtZ 1*-mбr~+C@R[mǃHk]1L`N'`sq$sƚ\ƁBUpSE$!p& [P~&IjPi!Cn%RV܄"A5 ~iOjI0?7@U)ULGST Кa6zُ@t{b_jLK?to4J.d@醀#[_cj#m :h-ZgYd"GdNH9EZu#h#'-Py8F-j+QN>aAQ&qֱXngJ^0dCTjVvXpj qрC%H¸ie%eN23r'g\ʦ>'O eRblOlK57&>[$F S(G[wMs`>RCusUWhs 98Qfe,PY @%GIM fGr n ]K}B%d -!*0\He<l ׌hVhm@|cImi!,ZR$cq fSMDb?j"ZBR;idGz!h-n%zV.|Zݷ$swh:P^1ά44є{]B(|۞8(B2<>C#UoɪӹuBj}.c]>Y1d22MgFL~7vשFv3!RA|r`?:p$<lA MnHDĞfxIX}5jeo9å ZK3LwADM=1,7hH/:=qPbmIi;ȮZqa,+U<Ư:. =W!Fh!%f$̫0Pa1o*+.Ț@Oy(&hʲelA46@}F)}JCRDzPhjp-nb g ruH[+KךTȥ b6nia:ֈ "zP0^ ^]lCF{LTIPjrzE^DY62#k2 \XT Xкl EI2\! 7kk͑qDYHy,E;9^*žC|= FY@$QFKuruiL]lЬ0a`9aSgHnw33/G,:q"Y=P:uNDRc!gzZhי[r?V`~`xi-1Y^p텄l튺b*%2w/K!pU0Nee¼䨇)}:.ϧ%ZxICaE+iɿ!Y&GNOJNP2ct12e0 nyB^JJ P,V;QQ~\Mtval4#*t9v={B'(UXRr{e"bx* khdEB 0-`FNfs]2{ےQX_B $L2ͬqY jA*Gg0ᵒjhv+sdS P*T($SiWՓƴS0h5UXE]Ľ;>čyى0enЈf+W:%SU-߁j`9ڱhQPЪHq:ki'Zhezef9HrE8 t DHDh 3 ZuU %#oU 'R:XmjiU8#M No&m PùA2FȆ(i:؃^Z}!|+Zj.vT7ȚCiLXPm c6A MJ(ip(eapKK,ܽ7{* %+"~T?_swCDIֳSh# :Guf/XMY*E-#05Z=*-H!i@׌6dTF;iXH fJaht03}0)(? cv-}+7F3fgV1`7! wmsm@qP"dfGk,.]g!+duIX}>/"}m3(VO{{9n/$Jori$ݡGhl|g‰ـ(OT`En@sPEq& 9|Iڐ@n# U*hVHU.C w%v./;C 樾8%g44P Pj=FToT&$*Z2 is OG2;1sYK-C*ilh+3(ql{@˶PP'vNs<̼ppfJQMա{L>2:ݛ2N;aOA 5f~jd&(I3flC2P^_f1&FCI'bSdNuӰ/FЙ Cl@IkwJJN#. Lnx  g<ه|Lf xC#VpU񎺙qmse!--WH9RyH$ӌZI6<}]vk2@ U?6~ [itg6bYE\$y~s5Nȸd%Jc 0@\ `+5u-)/)`|GSkO8^<J `]lm{ yl \3~uYK 2Am{)T8 N8y\r4 9|n7JTL0tw\:Y]o 0Fnʿ@YO/YM*M)>H 8(b|3Β LO(Y>/# QKkӱo۔ }S\;"<[-l#QyErT!(͞X@-/4;>Eb^ah[)LvO&tum)QOfBt36u)}[ϒ{Ru,pd_4N%:LLA1Wt(ȶꕤ0xv)\$<*?f*B yN'{Kkm1iCpE|1F+jVĜ(a+8i%yvUr-JapreS~e9bltq_+ CO-b&Pv zYV{eѨIw%5J:sҦ Jukc'be~:xf(x"p4&u'O"ѨnHЯ]8Tп 9 >϶Y3ePt:,HE3.p&[iS^dBE8FP<-rGchQ-TRU.ڏ^ BKkFrU$ .Tyf{{(2Yaڽw>hFѱZNk(DZ~7³lbÄ0` FAk"3,20ì@"9pj0IJs0^p2t D*v SQ+o27w,l5ᆹo14 6QQ؋s" ;%m7nb 9Ey_A?mبWAB" z;Dr0&o>'e hP}܃xΰp<.q 8b;!prUg7 אn0I=HhHqH4A*(sr}Q6_WjdXK~i-*0]"<˨/fhjă.&c}ʳ%f*iRW$l׻u*\MdgA1멲 a1LdTCH+[}k%`XPD9! u?'y )󸪆 P0vN‡@M8([蕳sܪ(Ic)/oZ^g1`Ɵ͆, Na,R@{`13E7gtkD٬6ǏQ&v &La|%ĭf[`7i2Z868Q72ڂFG7vs-@\~Aj-j C'BbT_˕ud>.b$ʯ1#qx7P#FȺ#W,hC&"ϭ ! D@h 6`8XtD>@'srPg{h8p1$`J 왺N:HnqMxAei-o; 7SAUbҒ"!e3yVP7!HqȲ"DN sò"?J5pI|DCЮ|`m*+)/rύ7{1TPE9#eY#2:rQ m8ud볠,0٫Hap(Or/zېp`~1l .c6C"͈1&$aÄNs#ޒ/6mNY(۸@A:JEkkbô\7T7B8"o/îcJpŠ(ZƝDprHu3ċ-7hI  2v&E( @"H4Ebv )=IMnޣ&}@DApkvޚyOWk-{cB żMLc8Dqb*Gx:+5e@6䮝}]Bd0Ŭ%Tr0[ʛ;H b(eʙ'&;y\HVv_*9U]%ccH   wǚr [gN4Xtp=гXY" +ߧR%gʡSb#!#1x3x T耗'hCka @ky@ִ^R·:vqC0/2F~i=%p0&TV'# ݵ>σO8S@x%mwgQph9>%|iљx}[5 R@Tw00E&K\q0Vy>u[WGq*@lGCI"p#b5 )4Nn+bLRi+p8ym ا&!/Rb  LSQca%ideQb&f!+˱SӦ8TıO)> |`R9;)($I23K|0QaLчBk3%3rCj|| vjk͉.61Ã]F8U1 ]+F+D$D0[ z#C_ژHoH^ Rņ`M1B@">vˑ3&Ӏ9hZդHBD'p_md3@ENS~ (;{VWR'жhINDndMY2ET'n@h^ȯr(eFC!QaaL-'AD DArialSans MSnll 0"0DWingdings MSnll 0@DSymbolgs MSnll 0PDcmsy10gs MSnll 0"H?H?> LPe,cmsy10Regular1.1/12-Nov-94 cmsy10BSGP19"`WhKw~s h|h{f&`[ h%N#sv?)븳 jyҫwۑ][:׽G-+t\3G74+s`+/ н0ZwOUǜI"h-UäQS*HgkE$Q^q5> m$~Xq_r}>CՒM ?.zEPQhFd I]age 4d/r;BØ {'mҷ \bE FN/`q3HȀ7_Dw ifi9 v:'{3RGk AZStI@CC-%CA'-l4 jX.A^!ʘ&##(`Hpi3@^l*n 5iHF Mrxo!=Gηtj"̔(gܒ1'M8)[@ޞPuS=EYh`M )EfGm;RZsH\TxCjs@\ 5((PVV";|$K ȫ4=\BBʇu^K/^>Tҹy-4Ɖ5eQ zKD1q7-[4n|'r; Af=%?IK}-&L+Z$mPTfTfZ[Q8;#qSkxGdzihy-yY(+ǁ/Pk;j&je_ޝE?eE1%#!߁yFPrmZhpՉȠz3^/IrW{5]AWԪl~>eW}0BtP*ؠBGEܩw  tx~0 E L 7v598H?b{"<FZH9 1KF3:Uz!<&jn ֳNmYEof V,r).1e2\VauԝV%HGD̑H$ WP:Z0BJip`-yhi1%nsp/.ܕ]&^g !y@&gbi$0[;$j yGZ)d&xU0CYZ`$^;B@>&x #㪘95@ 'wɡN@y236sE򂨄Hc#aTd[XMn&)گO{e?XLazO _w'O]@VX‰Dlȳ vahJn Z_֖Q[#R+|S p$X0Xl>HWL\e4ᕑ`wMxYHԞ"۽ A(y1vdU)^kA$^j.v䔌C17@ע¨"Dc1U.䗯h -A6gmHhLv2^Hee\&(,fP_#dQ}BB蜔B街xpt ;;T2E~ja&4T:fҖW# h~$!&f>9 8~]UK01i;:::&+b׊dpUi/!ye_ri鱱1ៜyNIGY&NshHaAD/;(G r9NI]` CN4a'V\5,rFDDكly(痗[[a# HR.>)^ ylK)8#H3A(%ZQl@w4(m " "G& %8r=p 2v]+* _|*;io[ kFҌsX Ldt)Y-\E}|/V6' 2xmWEȻ|,no@Irzx@JJ4FgĀ]@$RVO(5߀w@7F//ϪteBF1C|;|̀b/@@v>T{>GljX''aNd4`9BSR q jav^P(Ә=4 a= KǜqJ,K+mDW|pRPۂ g5 zE0[Ƹb$!)qrScDӆ?}nr.P:? |{/dz5Õx efF5 yLzӭ. 6`2LFƣrF!CgGDK]x1[b| ^{NH@]r hYxoj +6)hBubI S##lC4P%)i j(6ue>RjΉpQlN᝱Z{F p+S{itYLӡjT-?RLaCjL5OSrG6n {>ge*F%Z*E +7s%$5/.lGb0'h^w=^"J_ ]4a^bz,4t&vWK,{#&b0͖y]C( vU8v+GR֣I!/F Ny҂N<2!hL*[=Xœ5M`sٖ`)VKBsNnVkˊE^iܟŻl\)ދz0`[ P/ e[T̈́^7q! 1F^ig1'ˁM{awX tq1?3oŇ[e@\B!4TA]f' -e@&CqbyIX@c4*Op@`&"= X@CC! neiy%exi0"ǔ]P`} a "Jm &ԣ&DVwҺ~ǑkN2Wm橱S^TV55ҡPg*)6q28nr"SzMj%F#GsS~ kjwJ(6;Y˃$}YpB߆.L0,Hv S07pDLr ?lh;,XJ 7ִ}IʋD #3XD ?,5rȚ˞ r4^H,!%xE{1VIi5K\X4s$6VmF#)j Mx Vc_oPp:_2# *2o|ՎcH!FBȕ"򒴫^7OTM,\#"x91CT0ՐY~obw!ʬe%TtVz.W璧,Wnz7)_㝄( FgHxΡ xN'1;rUp ((rt" 8}ҵ&=aQMIv{ CQȰVjo ud0ʥZRY{,.3HN⪈ϮaBi, U8!h] 3ΞϞեV5DvmvDRB*rTQ.mnfpkmPGU}CH,[(SFupf\2EDu=mL̑du#]b#ã,we{my2GzW_f0YN )%BHD@wA[X82mTw 2Zm)aZ3qeq?IY}MO*!." we,6MV^F%Q6cj%sh}Nق"A>4A"tlP.hbTGϟUtZE8+[1=un &a̴28a*2" b4B `'zlŨ#` 6ZPg+iGG."Fǡ~i'6Aoȼлlor>8EY#XFb߽h[x] -!ɎAhmee&&lΛvS2")m}~9:ՑaK.kQ">GTYpNɐu hU|}KvB]t]T$sz4 `Cn?uwܰ&pWa@ @3waqAM&@kϾnE j/s:? Z,4K" uɽWFRzT4Ɂ&MP2@T[mmH_^-^:>@s'=/iOt,( m/?,6x } 5Z07,^pQR';+O8 "Cڙ0pK K'"ਆz; *|3HdeȂ40"TuY:!sP`qE#$`& tUV$icV`p7ygpXU"0AR_l"}ȸ`2L&~M⡟؄.T`S[3:^C5UlqqyDj,><;+Ț35}v:Xoa A (vaU7D.G>9R #@I'\/=$%^VEY7ÓG;6 {E.[ڝh̋c|ulmj/BP,# ]Nx6`S#v@RiFAō4Vu꯺U?$mib^vxJzPfl/ eJG-TCsCљ8zng_psNlJFm_z&D6W\pjwx/899n9{OL#(ײ2|(B=zEoix ϘtCͥ! lU;ua7ʥ[3e'BHi„2:2Gڂ IO&':Qw C')6GcE9;(u6]NwdMH CVE-:8BfuCʏp1Xn"1PY"B[ς^wuHRa[S1eQP 6ʹ/?3.wGX ;QJ Ġ?(8ܶߩ:HVo tE-+AwiQͧLegKyN@}Ƥ*mH7i.̲_&|GqHzqD!D-XDʅ d]g^`Wɶe\qtڹܲ- p⠻>;z~ GnX:B(}KܩT"V[h@Pa $pk橘ôK%zco_im;q,M=,qcO.:fAUE5K"Pe(یB ^E'5v-e.a (R!2 7b7(nH'tH Pd z')h'bKv]SL%t]ZgS@>JGcLK2M"SZ~=ہB؋{tm(8KkY@ïH!m|Eb- O[P|m*c(g?n%R~4zIv“[5d y$YwThƈVD "طMkP`0lSgpidIQ5"Ҙ/*-Ds'iT@enwP8[gjSLkH%j.%6m!ACGDF1g} NY"02 >\E%2.h<6+M#KɃ# /O> ,{ܷ83-<gفd vDoٖ;p3a)# {eRPmb (WاVvOGLx`Vm +K?)lOIw A5G0l)6ŰbnHNڑ]׾A؁g[l{(yF2j :ö{#^ 'iY;CR>OMR;Km@aЭ番&hMhf5fzEYx%ğmMv *Qe>B +.6?hiPc=gg&|`qUNcEa (ZSOiO afnƯ)G4mrFHpPZ%EڢX=%~p&Il Z M (cAz֬z-A#Ċڲ1$0h&2 pbhו<n4+XHs@nH hcќ-`1He`_ڒLZ@NRr`@E)2 0ľJx oi]p84nu@ad(E+U evaj+Sz;B4D|myTH@uhʓͬ36p_DL y4%ڈفC$\%82}C.L~ Bn-t_C]v B>" 4*Jh9CRn%E΋uEue0@/ꕼ<k6\@'GeM)'Ps]/ƎWm P5N,9@W=`Hn= 4B4`F]Х$>lݥm?FP o| )bQcM ?ػ fr/U)g}(4Dw p\n$d/ 0zg.-`.3%6@ ğͻO7*,ҵ*b; Y[@]%} lR92Cۖ1D\VXfa/<:T)cڟb,q)bvXVqIV1 5]$4J݈ \$t |@CwL?% ыՄ /;-RB JM(:AqVUœˢu 4,6\݄8@]b`# [FE ,-?i}Y4|Kʊ0`(X) 2p@yrDrUeO}}$I_L8ߘ0WX+ ۋ VvQzOZ`tX>XThQ@0ӷVKJ\ۯOpYa^N‹;048)iFqظ~QREdz.1IdLL)(ab)Q$ՆBcx(-ۼ5[?/T0ZbBzx-WotA&jL2]EtDת[d.ged^sio؎1thU+5*ľA^Bq<7jD@Ay6gKAsz %䢟*{ r%H}tDS0PKHYe ]"O3Gs<%w,:[T 4MPOs!Cd+^ &R[ԶqfpɍO!TMz͚NlP( pXGpQx.d"mg SS}XGPEϻ'؇t7#0\~–fCCiv+boaKi} E7~ 1-%Ig?u߮,  ?睌F-MNS>+BeB><4p( J]ɧ)X}]]JH",6*#D2;;Sy~coNtHzFz?#Ev󽎳3"=5X&'p]wꨠdq J"䆲(ЊNh\[1FoqS2AFUsC^tZDL"2(Ha̤BWim>bQrdy/VMU$mlB9VM:y, $=|G4r1xm m/rt"*K1x\RDSs_$^8$(M&g]NW1 JW~nGӛS%>j+#;{-,7vkZz6;R~qPW cda%F3"#{RTSTZb#=T ?`P_ 0M+E3oB*<mD@SK(T;+Đ9o ?Ͼ} eeimy9ƍmx3vbCd0ʛʚ[j!@7d8f*4L2ev(iɏg Bb\NČ<33&$HLvP[Dž֝iplWF(˹$7ϭyK~A(jX&LCBKDA /ˊcHUJ:b*ZoY݈c0u 7"`+zP._2xjweKd2rQƷ9vŔ_û 3 S}­A:dUˆ- *#DgF"##oBАDRHcW$"dJ ,r9LNϒ XIHJݳ^e.6&HX-X&8iĦ`/# Qr+Ga$ s12L[7BMUn!3,Va#IaR-L]kar=+dAlp!^i ZZ'$̕txD3aר JR6%[ 4B%AD]W"@6P&(߶.1 ?7 ?.os;c%'i X`Qzr{WP4.3CW)~]DWSZ /]Oazg?%BᡩVEԩE!z/t@{g2qqv{%H"}aBaFHpѸ[r`JGIi0$U" 3B:At+ޡ1>"Z7U#랋/ CwqP ' cs_nWo-=sJ>b`-5㊺pqU)d+vݪGz6I۸7c%Hv|:D-֤s nA|y~SEB6 K-+2[Yc4)Ȁ}S(#js1hvΩ<a ע!ሰmڦq`!l^` p,!WcA8ZB/Q " ~""XSLE[Ki;o $ 5[^iS0k˭(9rx L@م5zT\bۈz lS oSr=|8:^ ^AL#"l8Jejz*ҒeX<~MoKۤ$ET(Rh ah d oT3 IUNީ8g,>7Lrg[w/PrcY%_nL.q 5L4% vb?( ډu'?|&^O)K$*C \2)ןfIbk։n>#K }L6"7Y%Bh^$n 4ћp$T, b*W7ֵ9epvzx-uBP"-;PA8Wy5F6և.Kk@V'ttYh%b7lZ %kl1 nŲ">g!d/ a)qf\^[cȑWB^önmPD`0ΐA=>;ba)л  Ҩ/srg$Pؖqlt9Fc׺ɇgfPRb̳Nr9ތH`Wyam3[!8ST @&yYDlƏTg>GIG|^l \8ļOďS9`,ȓun%R,"C(X5@DUq\ "rҙ-y0ee\d̀VP|]Į #[6 E97C?;a+JsB\lOadKfO"@I`LrKq U>h%io `4ؐv+ĻhBWŊ.+xP8=^v,X4$krO|p#O1R?[~dUv8 ,8fsK%E"pɻ-?ųrb } !O$*,((@mz݉O8w81]pP bbQIyGSB4]X::_ϟ cTX"LGa&\ϠU{r%AMn00(뽣ч,0S72 gyrT :4 y fˆYezs| 0"WD~G AOi71 ^'2?K#w*B^%+#1x"e@1V b'*ϼbO;˦0@搘G#D>3Ds`i (^bjS(+@0}]rr"[5h)HN\jCepp*8dkWpw+L K%vqTiVbJ&CV?P/K|Ҋea!QřViDDB A_&;DMxA((k]UXW# 'i ? /v$cX= R#[[.(&S1 1t7OvX,rj&ȪIuƗ!4V&H  j~#rI Nrp|f J! *$К8$_#tg{(((ښyHwt,7疒@q .Y0"eKG!G tcH6 F#,g2xjl;@4_+.ϴ!}R`4\Pˬq'O #ECRI.-A﫽[@WEV確Ro6F^:71h'2J1KQbJD oaEd;1:Z[:(ds66pp+pwpp`e`_`-a _ !T&0K#BF۹odp," +{%A! d'4M/joaD7EjUFh\hTUp N.f"5Elz[w`M.6mLZLrDXI"Khs? D!:m(b^SqK* 5?@~$ ۶.B;ecWh0SLEGieՈ֪x zy, iG)U`DSystemgs MSnll 0pDNewCenturySchlbkl 0  C 0(.2  @n?" dd@  @@`` B):)G  '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$&"3:U$$F$#* N!E 8 JAM&NO!  !+&!| $-'".,&' B'XW*-.+-- $)!)!)!}p    " *+%""(*+"/(""#$(:123467<=?A F   STU VYZ]^0e5fm)nopqrstuv$2$*0Z0;2% 9$r$`[@LȱqDt9b$HeĖ8Ab$Dor#&PoSZG"$[9KfD7כL-'N$"$iKe&hţ׀PXxIg'U"$gw@kP}|'[ 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 fff3@8'w y ʚ;5 +ʚ;g4=d=dn  0pp@ <4!d!d8k 0l~<4dddd8k 0l~<4BdBd8k 0l~g4>d>d  0vp p2DEFAULTFONTSIZE10.DEFAULTWIDTH3540DEFAULTHEIGHT200E___PPT10% ``26___PPT9j{J2?> 2/11/2004 MSR TalkO =:w.Program Analysis using Random Interpretation//$ Sumit GulwaniProgram Analysis Applications in all aspects of software development, e.g. Program correctness Software bugs are expensive! Compiler optimizations Provide people freedom to write code the way they want (leaving performance issues to compilers). Translation validation Semantic equivalence of programs before and after compilation (difficult to trust o/p of compiler for safety-critical systems).?e>F?e [+y"Design choices in Program AnalysisTCompleteness (precision, # of false positives) Computational complexity Ease of implementation Soundness = If analysis says  no bugs , it means  no bugs . What if we allow  probabilistic soundness ? We get more precise, efficient and even simpler algorithms. Earlier probabilistic algorithms were used in other areas like networks, but not in program analysis. We obtain a new class of analyses: random interpretation.<11(Random Interpretation* = Random Testing + Abstract Interpretation Random Testing: Test program on random inputs Simple, efficient but unsound (can t prove absence of bugs) Abstract Interpretation: Class of deterministic program analyses Interpret (analyze) an abstraction (approximation) of program Sound but usually complicated, expensive Random Interpretation: Class of randomized program analyses Almost as simple, efficient as random testing Almost as sound as abstract interpretation,C\~          .   ,   A >    $   F       t Example 1 uExample 1: Random Testing v"Example 1: Abstract Interpretation { Example 1: Random Interpretation OutlineRandom Interpretation Linear arithmetic (POPL 2003) Uninterpreted functions (POPL 2004) Inter-procedural analysis (POPL 2005) Other applications `_ 6 Uf8Linear relationships in programs with linear assignments99 Linear relationships (e.g., x=2y+5) are useful for Program correctness (e.g. buffer overflows) Compiler optimizations (e.g., constant and copy propagation, CSE, Induction variable elimination etc.)  programs with linear assignments does not mean inapplicability to  real programs  abstract other program stmts as non-deterministic assignments (standard practice in program analysis) 3Vh3Vg 5Le#Basic idea in random interpretationGeneric algorithm: Choose random values for input variables. Execute both branches of a conditional. Combine the values of variables at join points. Test the assertion. t 2 2R0"Idea #1: The Affine Join operationAffine join of v1 and v2 w.r.t. weight w fw(v1,v2) w v1 + (1-w) v2 Affine join preserves common linear relationships (a+b=5) It does not introduce false relationships w.h.p.2)4m   l>t."Idea #1: The Affine Join operation0Affine join of v1 and v2 w.r.t. weight w fw(v1,v2) w v1 + (1-w) v2 Affine join preserves common linear relationships (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)D)4    >t.Q}'Geometric Interpretation of Affine Join m   Example 2[ We need to make use of the conditional x=y on the true branch to prove the assertion. [\Idea #2: The Adjust OperationM Execute multiple runs of the program in parallel. Sample S = Collection of states at a program point Adjust(S, e=0) is the sample obtained by linear combination of states in S such that The equality conditional is satisfied. Note that original relationships are preserved. Use Adjust(S, e=0) on true branch of the conditional e=0PW9W9 ,h-"Geometric Interpretation of AdjustaProgram states = points Adjust = projection onto the hyperplane Adjust operation loses one point.bZb5 ##Correctness of Random Interpreter RLCompleteness: If e1=e2, then R ) e1=e2 assuming non-det conditionals Soundness: If e1e2, then R e1 = e2 error prob. b, j : number of branches and joins d: size of set from which random values are chosen k: number of points in the sample If j = b = 10, k = 15, d 232, then error '*2z/         y               4Proof Methodology(Proving correctness was the most complicated part in this work. We used the following methodology. Design an appropriate deterministic algorithm (need not be efficient) Prove (by induction) that the randomized algorithm simulates each step of the deterministic algorithm with high probability. c)VOutlineRandom Interpretation Linear arithmetic (POPL 2003) Uninterpreted functions (POPL 2004) Inter-procedural analysis (POPL 2005) Other applications  $;$: 6 TgProblem: Global value numbering %  THow to  execute uninterpreted functions ?   Expression Language 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 Let s try linear interpretation6'Ak !A  N )Random Linear InterpretationxEncode F(e1,e2) = r1e1 + r2e2 Preserves all equivalences across a join point Introduces false equivalences in straight-line code. E.g. e and e have same encodings even though e e 9   WOutlineRandom Interpretation Linear arithmetic (POPL 2003) Uninterpreted functions (POPL 2004) Inter-procedural analysis (POPL 2005) Other applications E&D& 6 TzExample    Experiments  Experiments Experimental measure of errorThe % of incorrect relationships decreases with increase in S = size of set from which random values are chosen. N = # of random summaries used.F=U=4^OutlineRandom Interpretation Linear arithmetic (POPL 2003) Uninterpreted functions (POPL 2004) Inter-procedural analysis (POPL 2005) Other applications |lk 6 T/,Other applications of random interpretation Model Checking Randomized equivalence testing algorithm for FCEDs, which represent conditional linear expressions and are generalization of BDDs. (SAS 04) Theorem Proving Randomized decision procedure for linear arithmetic and uninterpreted functions. This runs an order of magnitude faster than det. algo. (CADE 03) Ideas for deterministic algorithms PTIME algorithm for global value numbering, thereby solving a 30 year old open problem. (SAS 04) $a$b b<KT 8XSummary /x678<Z[`bhjkz %&'(*+013;<>@DHIJKLP-   0` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@z?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>fL0 8(    6d "@  T Click to edit Master title style! !$  0, "0  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  0  "`  @*   0, "   B*   0$ "   B* ~B  Hp?"@@H  0޽h ? ̙33 Default Design   0` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@ z?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>fL0  8(     6d: "0  T Click to edit Master title style! !$  0 "@  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  0A "`  @*   0dF "   B*   0K "   B* ~B  Hp?"H  0޽h ? ̙33  1_Default Design0 0 @(    N`pr`r` )   x*  V++VV  N(ur`r`  )  z*  V++VVd  c $ ?w  4  Nt}r`r`  ZF  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  Tr`r` @   x*  V++VV  TЍr`r`  @  z*  V++VVH  0~dm.F ? ̙3380___PPT10.47L P 0(    N(9r`r` )   ^*  V++VV  NXBr`r`  )  `*  V++VV  TRr`r` @   ^*  V++VV  TWr`r`  @  `*  V++VVH  0~dm.F ? ̙3380___PPT10.47U& 0L0 5-  (   x  c $D`   x  c $x0p  R  s *\; ; \h   s ,,3 A ??F ]    0 ` 0  UUC-Berkeley March 2005"  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B +  0XL0 `x $(  x r x S @   r x S \  H x 0޽h ? ̙33___PPT10i.Р+D=' = @B +8    0`L0  " \(   x  c $D˩@     c $D̩<$@ 0  H  0޽h ? ̙33 . TIMING|52.|25.5 ___PPT10 .Р+EDr ' = @B D- ' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* b%(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<* q%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* q%(+  0}L0  6(   ~  s *U 0   x  c $X q  H  0޽h ? ̙338 TIMING|6.6|22.2|38.3___PPT10i.@+D=' = @B +v" % 0NL0 ! . J(     0 C"?6\ Ia := 0; b := i;0 2  0h C"?6? \ Ka := i-2; b := 2;0 2  0C"? o  l2c := b  a; d := i  2b;0 2  0wC"?$ J  assert(c+d = 0); assert(c = a+i)!0 2!6   0sC"?    l2c := 2a + b; d := b  2i;0 2F  S \EF  @ S \> L  @ c $$-X2  0 P F  @ S  I L  c $ 8;$RB  s *D77  0t:G @True 0 2  0G T AFalse 0 2  01 '  AFalse 0 2R2  s *EF  S  G' X  0d  <GEH@IE+E6^  6GHI+ 6X  0x d  <GAHsIA G ^  6GHI    s 0e0e    BCO DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| bgFNO  O @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab&7 ,$D 0z  p00   DA 4,$D 0B  HDo?"0@NNN?N p0B   HDo?"0@NNN?N p00  0E  @True 0 2  <4 ?"6@ NNN?N =* 0 2    < ?"6@ NNN?N  =* 0 2    B( @   H  0޽h ?@                            ̙33* TIMING|8.|4.2___PPT10.|0u+]AD~' = @B D9' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+ & 00lL0 x!!! (     0 C"?6\ Ia := 0; b := i;0 2  0C"?6? \ Ka := i-2; b := 2;0 2  04C"? o  l2c := b  a; d := i  2b;0 2  00C"?$ J  assert(c+d = 0); assert(c = a+i)!0 2!6   0\C"?    l2c := 2a + b; d := b  2i;0 2F  S \EF  @ S \> L  @ c $$-X2  0 P F  @ S  I L  c $ 8;$RB  s *D77  0̼:G @True 0 2  0XG T AFalse 0 2  01 '  AFalse 0 2R2  s *EF  S  G' X  0d  <GEH@IE+E6^  6GHI+ 6X  0x d  <GAHsIA G ^  6GHI    s 0e0e    BCO DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| bgFNO  O @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab&7 F  p00   DA 4B  HDo?"0@NNN?N p0B   HDo?"0@NNN?N p00  0E  @True 0 2  <0 ?"6@ NNN?N =* 0 2    < ?"6@ NNN?N  =* 0 2    B @    ! H ?"6@ NNN?N" _ ,$D 0  Need to test blue path to falsify second assertion. Chances of choosing blue path from set of all 4 paths are small. Hence, random testing is unsound. >1 2      H  0޽h ?@                            ̙33___PPT10i.|0u+>vD=' = @B +2 ' 0vL0 ##!'' g!(     6 s"~,$D 0 [a+b=i 0   6  ,$D 0 a a+b=i, c=-d 0     6? a,$D 0 F a=i-2, b=2 0  6  6, <\ j ,$D 0  a+b=i c=2a+b, d=b-2iB0 0 F  6A ^ ,$@ 0 }a+b=i c=b-a, d=i-2b40 0 F  6H%/C,$@ 0 Da=0, b=i 0    0(C"?6\ Ia := 0; b := i;0 2  0,C"?6? \ Ka := i-2; b := 2;0 2  0T/C"? o  l2c := b  a; d := i  2b;0 2  0,4C"?$ J  assert(c+d = 0); assert(c = a+i)!0 2!6   0X9C"?    l2c := 2a + b; d := b  2i;0 2F  S \EF  @ S \> L  @ c $$-X2  0 P F  @ S  I L  c $ 8;$RB  s *D77  0?:G @True 0 2  0DG T AFalse 0 2  0G1 '  AFalse 0 2R2  s *EF  S  G' X  0d  <GEH@IE+E6^  6GHI+ 6X  0x d  <GAHsIA G ^  6GHI    s 0e0e    BCO DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| bgFNO  O @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab&7 F  p00   DA 4B ! HDo?"0@NNN?N p0B "  HDo?"0@NNN?N p00 # 0OE  @True 0 2 $ <S ?"6@ NNN?N =* 0 2   % <W ?"6@ NNN?N  =* 0 2   & BY @   R ' H8\ ?"6@ NNN?Nw _  ^ Computes invariant at each program point. Operations are usually complicated and expensive."_1 2_  H  0޽h ?@                            ̙33JB TIMING&|12.8|11.2|41.5|2.7___PPT10.|0u+.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<* %(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<* %(+P+0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 +F ( 0tL0 E=@"!' (     0 L  @ c $$-X2  0 P F  @ S  I L  c $ 8;$RB  s *D77  0:G @True 0 2  0G T AFalse 0 2  0<1 '  AFalse 0 2R2  s *EF  S  G' X  0d  <GEH@IE+E6^  6GHI+ 6X  0x d  <GAHsIA G ^  6GHI    s 0e0e    BCO DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| bgFNO  O @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab&7 F  p00   DA 4B ! HDo?"0@NNN?N p0B "  HDo?"0@NNN?N p00 # 0E  @True 0 2 $ < ?"6@ NNN?N =* 0 2   % <̣ ?"6@ NNN?N  =* 0 2   & B @    ' Hx ?"6@ NNN?N _L   Choose random values for input variables. Execute both branches of a conditional. Combine values of variables at join points. Test the assertion. 8 2V-H  0޽h ?@                            ̙33___PPT10i.|0u+D=' = @B +  0aL0 ( (  ( x ( c $@    (  0 "6 ? `  " (0PpH ( 0޽h ? ̙33___PPT10i.0$ +D=' = @B +  0L0   $(   r  S @   r  S   H  0޽h ? ̙33& TIMING |41.6___PPT10i. LNM+D=' = @B +  0 nL0  0(   x  c $@   x  c $    H  0޽h ? ̙33___PPT10i.@+D=' = @B +> > 0PL0   %! (  x  c $@   /  <' ?"6@ NNN?N` 0 ,$ 0 Qw = 700 2      B ?"6@ NNN?N   6?"0@NNN?Np p,$@ 0 @ 6?"0@NNN?N ` p,$@ 0#z `p0  p,$@ 0   0C"?{!j _ a = 2 b = 380 200 (2 2   < ?"6@ NNN?N`p0#z  P   ` ,$@ 0   0tC"?   _ a = 4 b = 180 200 (2 2   < ?"6@ NNN?N Pz      p  ,$@ 0r  6C"?  Da = f7(2,4) = -10 b = f7(3,1) = 15#0  2  < ?"6@ NNN?N     <$ p0<$@ 0  " 0PpH  0޽h ?/@   ̙33> TIMING"|39.|8.5|7.7|28.1___PPT10.v+5!D#' = @B D ' = @BA?%,( < +O%,( < +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<*%(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' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 + @ 0PL0 %(  x  c $&@     < p0<$D 0  " 0Pp  <l ?"6@ NNN?NuE  Qw = 500 2      6?"0@NNN?Np   6?"0@NNN?N xF       I  p  6P^C"?  Ba = f5(2,4) = -6 b = f5(3,1) = 11"0  2  < ?"6@ NNN?N     <HA ?"6@ NNN?N` 0  Qw = 700 2      B ?"6@ NNN?N   6?"0@NNN?Np p @ 6?"0@NNN?N ` pF `p0  p  0JC"?{!j _ a = 2 b = 380 200 (2 2   < ?"6@ NNN?N`p0F  P   `    0PC"?   _ a = 4 b = 180 200 (2 2   < ?"6@ NNN?N PzF       p  r  6TC"?  Da = f7(2,4) = -10 b = f7(3,1) = 15#0  2  < ?"6@ NNN?N   H  0޽h ?O    ̙33> TIMING"|39.|8.5|7.7|28.1___PPT10n.v+z TDB' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+/ * 0L0 @8@ (   x  c $0cP@   B  0Doj ,$@ 0XB  0Do H XB  0Do4   <f@ 2  `  9a0   0N 9b0 LB  c $D    6W-rx ,$ 0 A a + b = 5 0    0v | ,$  0 =b = 20 B  @ NDo?"0@NNN?N n ,$@  0  0L{c   F(a = 2, b = 3)0   0< @ '  F(a = 4, b = 1)0   H ?"6@ NNN?N'pG .( 2L  H ?"6@ NNN?N @,$@ 0 b.: State before the join : State after the join/ 2/t  H ?"6@ NNN?N` L ,$@ 0  satisfies all the affine relationships that are satisfied by both (e.g. a + b = 5) Given any relationship that is not satisfied by any of (e.g. b=2), also does not satisfy it with high probability xb 2 2 2b [    fgֳgֳ?"6@ NNN?N0, 6"0( 2    Zgֳgֳ?"6@ NNN?Nw o   Zgֳgֳ?"6@ NNN?N K   Zgֳgֳ?"6@ NNN?N}  w ,$@ 0B   f,gֳgֳ?"6@ NNN?N~,$@ 0 :&0( 2    Zgֳgֳ?"6@ NNN?N V r,$D  0>   fTgֳgֳ?"6@ NNN?Nb(,$@ 0 6"0( 2  >   fgֳgֳ?"6@ NNN?N` F ,$D 0 6"0( 2    Zgֳgֳ?"6@ NNN?N` @ ,$@  0H  0޽h ? ̙336 TIMING|0.|0.1|0.|0.___PPT10.v+:Ds' = @B D.' = @BA?%,( < +O%,( < +D' =%(Du' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D ' =%(D ' =%(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' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* b%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D~' =%(D&' =%(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<* c%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 +9+ 00L0  @!)* U(     6P,$@ 0 I i=3, a=0, b=3 0   60|h ,$D 0 ?i=3 0   0 C"?0 Ia := 0; b := i;0 2  0C"?p  Ka := i-2; b := 2;0 2  0C"?   l2c := b  a; d := i  2b;0 2  0C"?Pf v "assert (c+d = 0); assert (c = a+i)#0 2#,  6p` @,$D 0 Ji=3, a=-4, b=7 0   6 ,$D  0 ei=3, a=-4, b=7 c=23, d=-23 .0 f  0C"? P  l2c := 2a + b; d := b  2i;0 2  6` ,$D 0 I i=3, a=1, b=2 0   6  0 P ,$D 0 Ti=3, a=-4, b=7 c=-1, d=1 0 F  S wWF  @ S  WL  @ c $X2  0 { F  @ S  " L  c $ PRB  s *Dp  6 ` ,$@ 0 Wi=3, a=-4, b=7 c=11, d=-11 0   04  AFalse 0 2  0$ 1  AFalse 0 2R2  s *PpF  S   X  01d  <G1HI1 ^  6GVHjIV 1 X  0 d  <G-Hr*I-  ^  6GHI "   0P&lF,$ 0 bw1 = 5@0 2  ! 0& P F ,$  0 bw2 = 2@0 2 F  p00 "  ~@ nB # HDo?"0@NNN?N p0B $  HDo?"0@NNN?N p00 % 0"+ @True 0 2 & 0""/  @True 0 2 ' <% ?"6@ NNN?N"   =* 0 2   ( <) ?"6@ NNN?N, =* 0 2   ) 6- @  Example 1 * H ?"6@ NNN?N , ,$D  0  Choose a random weight for each join independently. All choices of random weights verify first assertion Almost all choices contradict second assertion  2H  0޽h ?@                                333T TIMING8|35.7|2.2|3.|3.6|3.5|1.5|3.5___PPT10."(+^97&D' = @B DF' = @BA?%,( < +O%,( < +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<* %(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<* %(D' =%(Du' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*! %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<** 5%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<** 5k%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<** k%(++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+! 0 + I 0PL0   &` (  `~ ` s *K@    ` s *Qjv [i <$D 0  *(<)6=+7', ` 0DSC"?t& D a := x + y 0 2  ` 04XC"?`   M b := a( 0 2 ` 0^C"?`   C b := 2x 0 2  ` 0 HC"?  Iassert (b = 2x)0 2X2 ` 0  L  ` c $    ` 0 - AFalse 0 2RB  ` s *DL  ` c $&@ ` <`n@ ,$@ 0 Ax = y ?0 d ` <GH=I,` ^ ` 6GHI,` F `@ S   F ` S   H ` 0޽h ?o```````` ``` ``````` 3f3f"___PPT10._0m+uD' = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*`%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*`[%(+ J 0pL0 'hZ(  h~ h s *l{@    h s *,K   *(<)6=+7',H h 0޽h ? 3f3f0 TIMING|43.1|30.9___PPT10i.`2+D=' = @B +VK K 0yL0 0'pR(  p~ p s *v@    p c $܌G P(<$@  0  *(<)6=+7',  p 0  NAlgorithm to obtain S = Adjust(S, e=0) ('r p  `gֳgֳjJ?"6@ NNN?Na ,$@  0 p Zgֳgֳ?"6@ NNN?N ,$@ 0 p Zgֳgֳ?"6@ NNN?Ns(l,$@ 0 p Zgֳgֳ?"6@ NNN?N- B m,$@ 0  p Zgֳgֳ?"6@ NNN?N P ,$@ 0  p Zgֳgֳ?"6@ NNN?N8 ,$D 0B  p s *DjJuL H,$@ 0(  p B ?"6@ NNN?N %,$ 0 DS4&( 2 (  p B ?"6@ NNN?NI i ,$ 0 DS2&( 2 ( p Bԧ ?"6@ NNN?N F ,$ 0 DS3&( 2 ( p Bܦ ?"6@ NNN?Nc ,$ 0 DS1&( 2 , p B ?"6@ NNN?NP ,$ 0 HS 3&( 2 , p B ?"6@ NNN?N _,$ 0 HS 1&( 2 , p BԺ ?"6@ NNN?NC c ,$ 0 HS 2&( 2 B p@ 0DjJb  ,$@ 0B p@ s *DjJ ,$@ 0B p@ 0DjJ* ,$@ 0B p@ s *DjJ ,$@ 0B p@ s *DjJ 4) ,$@ 0V p HT, ?"6@ NNN?Nr" ,$D  0 lHyperplane e = 0&( 2   p Zgֳgֳ?"6@ NNN?NG( l ,$@ 0 p 0?"0@NNN?Nu B p <DjJ?"0@NNN?N& @,$D 0B p  fgֳgֳ?"6@`NNN?Nk ,$D  0 :&0( 2  H p 0޽h ? ppp 3f3f0j TIMINGN|21.7|8.4|4.9|4.8|16.5|4.4|2.7|26.2|7.50___PPT10b0.fw1+ab Dv.' = @B D1.' = @BA?%,( < +O%,( < +D' =%(D}' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* p%(D' =4@BBBB%(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%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* p%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p@%(DY' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(Dq' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(Dq' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* p%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p@b%(++0+ p0 ++0+ p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 +" L 0p+L0 LDP'x(  x~ x s *@    x c $`U<$@ 0  *(<)6=+7',F x  pA ?txp_fig"6@ NNN?N_ 8j h$D  04 SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $\frac{1}{2^{98}}$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False*RESOLUTION300"TIMEOUT156BITMAPFORMATbmpmono8 DEBUGINTERACTIVETrue&ORIGWIDTH906PICTUREFILESIZE2062 x  pA ?txp_fig"6@ NNN?Nm  $@ 0 SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $$(2d)^b\left(\frac{j+1}{d}\right)^k$$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False*RESOLUTION300*TIMEOUT (none)&BOXWIDTH354(BOXHEIGHT200"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG FalseD*ALLOWFONTSUBSTITUTION False6BITMAPFORMATbmpmono0ORIGWIDTH140.8758PICTUREFILESIZE 15566d x jA ?txp_fig"6@ NNN?N> m $D 0X SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $$\not\Rightarrow$$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH354(BOXHEIGHT200"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG FalseD*ALLOWFONTSUBSTITUTION False6BITMAPFORMATpngmono&ORIGWIDTH206PICTUREFILESIZE1386H x 0޽h ? 3f3f0 TIMING|17.5|42.7___PPT10~.(`+9DR' = @B D ' = @BA?%,( < +O%,( < +D| ' =%(D$ ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*xFo%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*xp~%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x'%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(+  0L0 `$$(  r  S ;@   r  S <0  H  0޽h ? ̙33___PPT10i.%2+D=' = @B +  0p$L0 X z(  X x X c $D@    X  0E "6 ? `  H X 0޽h ? ̙33___PPT10i.0$ +D=' = @B +:  0L0      (   r  S (K@   #  <`L ?"6@ NNN?N3{ y%a := 5; x := a*b; y := 5*b; z := b*a;800 Z200 22&    <U ?"6@ NNN?N x,$@ 0 .a := 5; x := F(a,b); y := F(5,b); z := F(b,a);800 Z2'00 22/  , !l    o ,$@ 0B   <D?"0@NNN?Nl    < ?"6@ NNN?N  G Abstraction 0 2  i  <L_ ?"6@ NNN?N  ; x=y and x=z Reasoning about multiplication is undecidableF 1 2/1    ;  0 s  <lc ?"6@ NNN?Nt  ,$ 0 A only x=y Reasoning is decidable but tricky in presence of joins8 1 281  B    < ?"6@ NNN?N_ X  0li  a~,$@ 0 Axiom: If x1=y1 and x2=y2, then F(x1,x2)=F(y1,y2) Goal: Detect expression equivalence when program operators are abstracted using  uninterpreted functions Application: Compiler optimizations, Translation validation   j / IH  0޽h ? ̙33 6 TIMING|38.2|7.7|37. ___PPT10d . e`+T+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' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* 2%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* 3%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+p+0+ 0 ++0+ 0 +  0PL0 ;3%` #(  `  ` 0C"? 0 !  "assert(x = y); assert(z = F(y));  #0 2#6 ` 6?"0@NNN?N?-x  ` @ 6?"0@NNN?Nx  X ` 0p> ` <p ?"6@ NNN?N =* 0 2   ` @ 6?"0@NNN?NW`~ ` < ?"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а  ,$@ 0 :.Typical algorithms treat f as uninterpreted Hence cannot verify the second assertion The randomized algorithm interprets f as affine join operation fw ,Z)Z&ZZ)$  m ` 0@C"?? x := a; y := a; z := F(a); *0 2  ` 0HC"? Q  wx := b; y := b; z := F(b); 0 2 !` 60  @ Example "` 0O_& @True 0 2 #` 0E  AFalse 0 2 $` NG&5H I&5?"0@NNN?N-p %` HG H$I ?"0@NNN?N> H ` 0޽h ?_` ` `  ` ` ` ` ` ` ` $` ` ` %`  33lJ TIMING.|36.6|21.2|7.8|4.2|42.4___PPT10."(+D' , = @B D' = @BA?%,( < +O%,( < +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<*` '%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` '8%(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` ,%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` ,U%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` U{%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` {%(+ 0 00L0 P4 $(  4 r 4 S P@   r 4 S 0  H 4 0޽h ? ̙33& TIMING |26.3___PPT10i.}`1+D=' , = @B + ' 1 0 L0 "" ##  (   r  S @   r  S L  }  0h  Pp,$D 0 Problem: Scalar multiplication is commutative. Solution: Choose r1 and r2 to be random matrices and evaluate expressions to vectorsJA  ;P F k-    M    H@ ?"6@ NNN?Nv AF$0 2     H ?"6@ NNN?NmV  AF$0 2     H ?"6@ NNN?N  AF$0 2    B 6?"0@NNN?N   6?"0@NNN?N    <?"0@NNN?N   Ca&0( 2     <?"0@NNN?N   Cb&0( 2  f3   <?"0@NNN?N   Cc&0( 2  f3   <?"0@NNN?NW -  Cd&0( 2    B 6?"0@NNN?N     6?"0@NNN?N R   B 6?"0@NNN?NB     6?"0@NNN?N   %   H ?"6@ NNN?Nk ge =H0 2      7 8  D  #  D    B ?"6@ NNN?N AF$0 2     H  ?"6@ NNN?Nt   AF$0 2     H ?"6@ NNN?Nt  AF$0 2    B 6?"0@NNN?NGgt    6?"0@NNN?Ngq t    <?"0@NNN?N$ D  Ca&0( 2     <?"0@NNN?NL$ "D  Cc&0( 2  f3   <?"0@NNN?N<$  D  Cb&0( 2  f3   <?"0@NNN?N $ D  Cd&0( 2    B 6?"0@NNN?N} G$    6?"0@NNN?NG $   B 6?"0@NNN?N q $    6?"0@NNN?Nq ' $   !  H! ?"6@ NNN?N@ b e =<0 2    n " <* ?"6@ NNN?Nk   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 ?                                   ̙33N TIMING2|20.|18.9|8.|2.|20.5|28.2___PPT10n.#+ksDB' , = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* /%(+  0L0 ` z(  ` x ` c $P_@    `  0_ "6 ? `  H ` 0޽h ? ̙33___PPT10i.0$ +D=' , = @B +   00L0 !% ;(   x  c $b@     0nC"?@ Ka := 0; b := i; 0 2  0yC"?  Ma := i-2; b := 2; 0 2  0}C"?   n2c := b  a; d := i  2b; 0 2  0DC"?P` P b&assert (c + d = 0); assert (c = a + i) '0 2'  0C"? $  2c := 2a + b; d := b  2i;60 2F  S WF  @ S 1WL  @ c $dX2  0  F  @ S    L  @ c $ PRB  s *Dp  0(`@ @True 0 2  0lK` AFalse 0 2  0CC AFalse 0 2R2  s *PF  S   X  0}#ald  <G+H@I+#^  6G HI a1X  0dNB d  <G0HFYI0 ^  6GIHIIN    H8 ?"6@ NNN?N` = sThe second assertion is true in the context i=2. Interprocedural Analysis requires computing procedure summaries.  t1 2t23  0`@ @True 0 2  < ?"6@ NNN?NTD =* 0 2   ! <x ?"6@ NNN?NpRB  =* 0 2  F  p00 "  `0 PB # HDo?"0@NNN?N p0B $  HDo?"0@NNN?N p00 % 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*H  0޽h ?@                           ̙33$ TIMING|7.9___PPT10i.|0u+D=' , = @B +6H 0`kL0 E=&((X(  X X 6ԵT ,$@  0 Ni=2 .0 f X 6к```,$@ 0 Da=0, b=i 0   X 0C"? pF Ia := 0; b := i;0 2 X 0C"? 0 F Ka := i-2; b := 2;0 2 X 0C"?` Ppl  l2c := b  a; d := i  2b;0 2 X 0C"?x6 & "assert (c+d = 0); assert (c = a+i)#0 2#, X 6\:* ,$@ 0 Ja=8-4i, b=5i-8 0   X 6 H ,$@  0 ^"a=8-4i, b=5i-8 c=21i-40, d=40-21i  #0 #  X 0 C"?` @ l  l2c := 2a + b; d := b  2i;0 2  X 6@ `,$@ 0 F a=i-2, b=2 0    X 6   ,$@ 0 Ya=8-4i, b=5i-8 c=8-3i, d=3i-8 0 F  X S F7F X@ S FY L X@ c $ ?HX2 X 00 ;k` F X@ S l d7 L X c $` SWRB X s *D"  X 6 CP ,$@ 0 \ a=8-4i, b=5i-8 c=9i-16, d=16-9i !0 ! X 0@$ M AFalse 0 2 X 0B  AFalse 0 2R2 X s *0` F X S l `B7 X X 0pd X <GCH HICHp ^ X 6G HI H X X 0d X <G-HI-g`` ^ X 6GPH'IPg`  X 0,,$ 0 bw1 = 5@0 2   X 0\  ,$ 0 bw2 = 2@0 2  !X 6  `P0 :&Idea #1: Keep input variables symbolic "X H ?"6@ NNN?N`  ,$D  0 Do not choose random values for input variables (to later instantiate by any context). Resulting program state at the end is a random procedure summary.  2 #X 6= ,$@  0 ]a=0, b=2 c=2, d=-2 .0 fB $X <D?"0@NNN?N 0  ,$D  0 %X 0@M @True 0 2 &X 0 ~ @True 0 2 'X < ?"6@ NNN?Nj =* 0 2   (X <L' ?"6@ NNN?N @  =* 0 2  H X 0޽h ?@XX XXXXXXXXXX XXXXXXXXXXXX XXX X XX 33\X TIMING<|49.7|2.|1.1|10.2|0.6|2.4|19.7___PPT10."(+MDx' , = @B D3' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* X%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"XX%(Df' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*#X%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$X%(+0+0+X0 ++0+X0 ++0+X0 ++0+ X0 ++0+ X0 ++0+ X0 ++0+X0 ++0+X0 ++0+ X0 ++0+#X0 + ; 0TL0 0%0(  x  c $=@   x  <A ??ll  H  0޽h ? ̙33___PPT10i.-f+D=' , = @B +@  < 0TL0 qiP% (  x  c $@   x  <A ??ll  x  <A ??y)~|   <DB ?"6@ NNN?N `P,$D 0 d Randomized algorithm discovers 10-70% more facts. Randomized algorithm is slower by a factor of 2."e1 2e  F  q   q  6?"6@ NNN?N g    6?"6@ NNN?N   <F ?"6@ NNN?N q a# Randomized Deterministic"$0 2$  H  0޽h ? ̙33_W___PPT107.-f+@D' , = @B D' = @BA?%,( < +O%,( < +D' =%(Du' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*3e%(+0+(+ 0+L- D 0#L0 ++P&44(n+(  (x ( c $HT@    ( c $Z  " (0Ppz Pq  (# #"&P  ( Ba ?"6@ NNN?Nf R q  I0 @` ( Bk ?"6@ NNN?N R f q  I0 @` ( Bt ?"6@ NNN?NR q  I0 @` ( B@z ?"6@ NNN?NPR q  O6 @`  ( B ?"6@ NNN?Nf 3 R  I0 @`  ( Bz ?"6@ NNN?N 3 f R  I0 @`  ( By ?"6@ NNN?N3 R  I0 @`  ( B ?"6@ NNN?NP3 R  O5 @`  ( B ?"6@ NNN?Nf  3  I0 @` ( B ?"6@ NNN?N  f 3  I0 @` ( B ?"6@ NNN?N 3  K0.2 @` ( B8 ?"6@ NNN?NP 3  O4 @` ( B| ?"6@ NNN?Nf   I0 @` ( B ?"6@ NNN?N f   K3.2 @` ( B8 ?"6@ NNN?N   L64.3 @` ( B| ?"6@ NNN?NP  O3 @` ( B ?"6@ NNN?Nf  L95.5 @` ( B ?"6@ NNN?N f  L95.5 @` ( Bd  ?"6@ NNN?N  L95.5 @` ( B0 ?"6@ NNN?NP O2 @`B ( <o ?"0@NNN?NPB ( 61 ?"0@NNN?NPB ( 61 ?"0@NNN?NP  B ( 61 ?"0@NNN?NP3 3 B ( 61 ?"0@NNN?NPR R B ( <o ?"0@NNN?NPq q B ( <o ?"0@NNN?NPPq B  ( 61 ?"0@NNN?Nq B !( 61 ?"0@NNN?N  q B "( 61 ?"0@NNN?Nf f q B #( <o ?"0@NNN?Nq  $( <L ?"6@ NNN?N H  AS$0 2   %( <" ?"6@ NNN?N   AN$0 2  B &( <D?"0@NNN?N6" 6B '( <D?"0@NNN?NC CB ((@ <D?"0@NNN?N`n B )(@ <D?"0@NNN?N _m + *( <' ?"6@ NNN?N+1 EThe experimental results are better than what is predicted by theory. F0 2F  j 4(S +(# #"  ,( BP. ?"6@ NNN?N4(S a231, @` -( B0 ?"6@ NNN?NR4S a216, @` .( BJ ?"6@ NNN?N4RS a210, @`B /( <o ?"0@NNN?N4(4B 0( <o ?"0@NNN?NS(SB 1( <o ?"0@NNN?N4SB 2( 61 ?"0@NNN?NR4RSB 3( 61 ?"0@NNN?N4SB 4( <o ?"0@NNN?N(4(SH ( 0޽h ? ̙33. TIMING|48.|55.4___PPT10i._+D=' , = @B +  0pL0 P x z(  x x x c $tU@    x  0 "6 ? `  H x 0޽h ? ̙33___PPT10i.0$ +D=' , = @B +  0fL0  $(   r  S s0@   r  S t   H  0޽h ? ̙33___PPT10i.V &+D=' , = @B + 3 0fL0>2/11/2004 MSR Talk ~v!{Q (  P r P S @   d Xx  yQ  #"  P  B  ?"6@ NNN?Nx  YAffine Join, Adjust @` P  Bș ?"6@ NNN?NX [Linear Arithmetic @`B P  <o ?"0@NNN?NXx B P  <o ?"0@NNN?NXx B P  <o ?"0@NNN?NXXB P  61 ?"0@NNN?NB P  <o ?"0@NNN?Nx x  !Q <d ?"6@ NNN?N  0Lessons Learned Randomization buys efficiency, simplicity at cost of prob. soundness. Randomization suggests ideas for deterministic algorithms. Combining randomized and symbolic techniques is powerful.J0 21 2    d Xx  wQ  #"  &Q  B ?"6@ NNN?Nx  MVectors @`. 'Q  BT ?"6@ NNN?NX vUninterpreted Fns.  @`B (Q  <o ?"0@NNN?NXx B )Q  <o ?"0@NNN?NXx B *Q  <o ?"0@NNN?NXXB +Q  61 ?"0@NNN?NB .Q  <o ?"0@NNN?Nx x 7d Xx  vQ  #" 6 2Q  B ?"6@ NNN?Nx  ~Symbolic i/p variables   @`/ 3Q  BP ?"6@ NNN?NX  wInterproc. Analysis   @`B 4Q  <o ?"0@NNN?NXx B 5Q  <o ?"0@NNN?NX x B 6Q  <o ?"0@NNN?NXX B 7Q  61 ?"0@NNN?N B :Q  <o ?"0@NNN?Nx x 0d }  {Q  #"     \Q  B8 ?"6@ NNN?N}  TKey Idea   @`B ^Q  <o ?"0@NNN?N} B `Q  <o ?"0@NNN?N} B aQ  <o ?"0@NNN?NB eQ  <o ?"0@NNN?N} } H P 0޽h ? ̙33___PPT10i.y`P+D=' , = @B + 0 0 4(   d  c $w     s *٭ ZF    H  0~dm.F ? ̙33 % 0 h (  h X h C w    h S  ZF    H h 0~dm.F ? ̙3380___PPT10.P!  0 0 (   X  C w     S  ZF    H  0~dm.F ? ̙3380___PPT10.n˅  0 @ (   X  C w     S d ZF    H  0~dm.F ? ̙3380___PPT10.?'  0 P (   X  C w     S   ZF    H  0~dm.F ? ̙3380___PPT10.?P  0  (   X  C w     S x& ZF    H  0~dm.F ? ̙3380___PPT10.u0،c 0 \ ((  \ ^ \ S w    \ c $@, ZF    H \ 0~dm.F ? ̙3380___PPT10.?P 0  d ((  d ^ d S w    d c $0 ZF    H d 0~dm.F ? ̙3380___PPT10.?P 0 ` | ((  | ^ | S w    | c $6 ZF    H | 0~dm.F ? ̙3380___PPT10.?P z 0   (   X  C w     S < ZF    H  0~dm.F ? ̙3380___PPT10.y wX  0   (   X  C w     S dA ZF    H  0~dm.F ? ̙3380___PPT10. %  0 ! (   X  C w     S ,G ZF    H  0~dm.F ? ̙3380___PPT10. I e 0  ! (   X  C w     S L ZF    H  0~dm.F ? ̙3380___PPT10. W 0 0" ((   ^  S w     c $R ZF    H  0~dm.F ? ̙3380___PPT10.n˅  0 #<(  <X < C w    < S X ZF    H < 0~dm.F ? ̙3380___PPT10. ߉  0  #@(  @X @ C w    @ S T^ ZF    H @ 0~dm.F ? ̙3380___PPT10. Ў  0 0#D(  DX D C w    D S d ZF    H D 0~dm.F ? ̙3380___PPT10. +:  0 @#H(  HX H C w    H S i ZF    H H 0~dm.F ? ̙3380___PPT10. T } 0 `#P(  PX P C w    P S j ZF    H P 0~dm.F ? ̙3380___PPT10.   0 p#T(  TX T C w    T S  t ZF    H T 0~dm.F ? ̙3380___PPT10. 0oԊ  0 #h(  hX h C w    h S \z ZF    H h 0~dm.F ? ̙3380___PPT10. T  0 #l(  lX l C w    l S 4Y ZF    H l 0~dm.F ? ̙3380___PPT10. VY X 0 #t(  tX t C w    t S ̄ ZF    H t 0~dm.F ? ̙3380___PPT10. _ 0 @%((  ^  S w     c $ ZF    H  0~dm.F ? ̙3380___PPT10.` O 0 `%((  ^  S w     c $$ ZF    H  0~dm.F ? ̙3380___PPT10.` O 0 %((  ^  S w     c $ ZF    H  0~dm.F ? ̙3380___PPT10.  0 % ((   ^   S w      c $ ZF    H   0~dm.F ? ̙3380___PPT10.  0 `&,((  ,^ , S w    , c $У ZF    H , 0~dm.F ? ̙3380___PPT10. [ 0 &\((  \^ \ S w    \ c $ ZF    H \ 0~dm.F ? ̙3380___PPT10.  k 0 'd((  d^ d S w    d c $@ ZF    H d 0~dm.F ? ̙3380___PPT10.  0  'l((  l^ l S w    l c $  ZF    H l 0~dm.F ? ̙3380___PPT10.  3 0 @'t((  t^ t S w    t c $ ZF    H t 0~dm.F ? ̙3380___PPT10. Н7 0 `'|((  |^ | S w    | c $ ZF    H | 0~dm.F ? ̙3380___PPT10. `=x\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;ΎophPx lޝ;'N!!> bW0 N|I8vjoDBUA%-B-HUDD T8U \{3>_G$vg޼y͛f>V/9 p.Yy.@RsdP`}B /,5@,0a)in~ٴ9%]):]ӳa.Gen?z! ~'` A}@H6@>'nWqM< eK)[Pxx[|̥K7n&fޠHw/5&m[STw4wZs-n݊wBTq)U7vtv]H!Bi|w[̆qYԛO}fܷQ%5 ZZܧK4?qݭy޶[[e&<֭],s龭6!ĝs^>^?{P6-P:TVGOq\K-B+M(~(WL>( MM$ʅ_JM;?Έo.Ѽ|ظL!j +pztM-RSv#9iiҌzeJ;kk=ݎN59ø?X~,o V\$f9˕;viAO?v0~}am 5h;eș!{.\Adžs yvJv2XlR, -.uE¼e"d!ugnfŲRٮ)67,vI,vFmX J\_C&~|+*5ʢUDڇʣ|6ݭ[.sU#N>,x +D\+wp.Ig~}I + F,C^$cھge y M|#jco{iu[fD"U[F*m&&vwYVזW~H&.&Qܽ8tF._3$0468 e?ꋗL9\Ժm[-{\3kf™y/}mhAk0P^:6C S|?@k FNn^f1A68,_c7#=!y"?^)n{# oIfYu_-_5XL6N,.\I1|ڕu^mĘ0~j; m NA}ֶf>c텴]'Z_;]cBi`B#RCVa>WFS.=;uWڞi0?0ucJE1lҌI6Wo MoKTѬ*/,e~*7Ez`3᧙vϪT:e3˸6΂J:H\nmkQ3ݙ겮.JNNv^{ OMgΩws MnLMtBwtmGM &;#WxW~ZZ,D߇'t7P~އOǯ+婣s”v¬T.Lx}9O]`wDOaI@/ "{EBc-|w[ۘ2'F~&O)#IB >&|Q"=t~+ ZЏtN?02Cx[z_ߢ=UaѮN)pgwdVП5 OE gI#Ws%:Ӆ'kn/mX\^(&܁t&/=Em^/Ltu .5WǤ&D[n)"I"],,pVQjsڕ֐_# ɦʌSSW6r&I8à6ZQ-nV`8;V` +E_2# H};Q}q$.d^!U-0Uom Z Ϋ:RbMLbRycZ0)Ƹ $bq&)Lfi,B- <o?/S (^[6(_̲8ygxU[mf4O݌I)2 wqM0K+僺 Mx펮fڔED^o/"+U~,BRLwD+ M[ǘ(=(bS,e kO]#FyY&砇4LRK{*_򒜤Aۑ([ rME5p^jGJ>6#:Y3;VЇR4y%RA%RDE%FE>Ҽ ;^6{~D5^^irK5zRqgp# 4{s3:@m&a?s`m{0]AwtG<O}Ǔu:A7CAg2 /ɐ9ۀ$~,d x砉ta6 h7}!ͳh:͗`{ǡlޢK 6u|P怷t8%@R6_XH(`'u+克55AO^P^xmd tz /ҝS =b养\?bT?F?םǓmi]r=.g~xz}yd'uw>+}h:gP}aZ "E>F gO\q*-ň s/*x */T ׹Jj{ˏg|~<ԻxIsߏSn3t |4D^X9Z\~aUr"Ð!&O3F)Rx lGޝ;6NRձim|$j]K|I8v7)^BJ[-T *%B4) AS(>{3Q̛7o̼yΞO^}ꩯO; 02N hv)p*"T!5._Z? Lh>)ț&p+ptbt1?Oφ9|B׸i=Ԣq z z!QN & W!c/?= ס6vv}`@I;qgenGr,@s A"T"!TP2L9t`2#@0 a60a.<cϥ 4&`4=BBP>|:0g۳}yx+/+=vk,C-`qYHzENo'ۧ5$@TvzGh@Xab%".EhBhFX2ˁ`+DJl aԘp:^쵟=d:,\γ4W TEćnܥ^)y\қJ~:AtjDo՝⤛2T Iw;%t)m}k9Y*. orxHPhߦDۛjz֋!fdQZ?u}W>_4ϩ>rϮWooQ{kioǝX浇{?{v[v'zY?췴Ww&/Ƒ۱A6קpڶDe{6>ul(ա1kE@l"܄rQrNhȔ郢BRNHt4sSL ˿Y_,$ջā 'rS r )iYFK2LkC':ּ@^@ F`arH5H"1Y N lӏ{5O8!?>rY63h;eY!{h_g[s9{¼en ,[\^4yv j`arqؚJ#mj)p8m Xv*uv8ŲSٮ;-:`b٩lmւ`T.d=Ch2G JЏByQsk@z5qG4﷗(`n37hn䖲9npp786\K{;I yv wL-ʫ0w ys=fOߡ֠9h%h=4a+qŞ}ݦoJEWTanԉ'7h]iK|l[)ӾK #p>޳REm:Έ?>ñݓH_3R& +$`8˸v/29={Z%\ή8~RHڕ3*t wCʏXP(sl)FCGzBBY8#PګPgtDH/WD:_/*bs+;ɧZ-_U7ͯheoSvdH@z/phD@"G=y9_|nN] J!ez`7ЉT}0/\=o皋z0kϥXY\Ә:W<_3MM1vsw6쪷 ] sؑKT{fhIZ?"G LgUWۈŵ\ۉM@HYnmk 赱3)?ekkeN;3gO-^ָnL]̃L?:{tc&ᅍ?[^+x^5f 9rdœs]w͍-붽Ysi _:{CtA# K?7# M]Y&:הVuCҩV.vFlo-x.}v@q7[1ҏDOixfiQbg:DʡPePm&|RC&-Cґ&yI`o[F d)O(C@0o@ڂʤFa ơ#C(a3Ea] b?!KŮsaьp:} J3HZkK_\37L4R!˧ul} &23- 1hlm=_7ކ z[EGpŸijO إ۰EA@ ~ǿ#܏t&oCpEma&b cR eJHҊj鸋]kuA~5TvjBvr*]8q^$ɛ}Ԧ**ŽR+탺 9]uPyeED_nUVX)U"Pq1EQ(Lסgނ-Ck AjdnzW $'iv4q7&梚I*UJǠ6džN]02*[hh[})FN)9DD%ƉzgH62( zHK95!M&M1~|!Q g0_=Dn  UYc/Ƃn;cbOaO<*O@n Or;ڃQ2)}4\@[*HހwȠ;q⿅4ϠGa;BުQލsŸBA mJMր6Tdi'N<ℵcam-% #kjf!<)&dzBy-1/<3ycbOz m<!O;)UzJ witSJx3E*ӳo=+NmjxFgOƳoϾTy="群Qu^̞}|={X=ʬы$= :ũڷH# R0q 4TØ? k]~|3[2x3MZ}~Fy,oK)hT풴Ӱ;E!{ CO =Aq.!s-??Y2wpjR~(,w\F@엗 籏|q&?d~☏sٮ\\ ☏sٮ;*☏sٮ[8\2w,;mbX qvݏD;g٩uP$Pxklq?ߝω~}8!qC|yIIipKĎψgQ$Z*<&VGE%iAj)(jPkTũR:3;)=~>5m 'vF!;N  gUƓ_4c Ѓ~0n/CI SdxBp6?O{9!ݸV?ypa˂8  Q(v& *` Sp} !:+0P髰>؋yjbVzĿP,¼HQ1% / P<L)Ӊ@:0S1N8 318`qp惦f$)h&&!hquC=qs Љ}CЪR.}uB;0~ny>./pڷe@wZ?[j 0q!Ek0.Hzz:K0.Ÿ //T}XckNƄyxfqt8wOW TY65 [nܥTҥw:Ae&ѷ7ѕiQcm lYۤ-d\ɵίKs}STf)WMR$O*iHP`ƶDܶoWB*Z)杙?ؐJwnm(g$?89{)ȹz-ȹx}.y8'o-ww\uC۾N9ƴ'ٳl=<>>gO7PFnuAIG%r,JeuB{R:XQB{Hi*aBC%քrB9uzƠљ< 9Go &aBQ E7Tszu}Go$%-+@RONT_}=:@fbIg[+*2kTҕz.}ޖPzq&D51zI[yHϒȚ!{9 v,=jo|cI[evpLb:yYG9&1U6_5Nr>{?,M 9HgG6CIV qL2ʎ IV:2$N|3d&cH0#z(s5iX3fi(K>kk{;͖}I2r4xgldÚlX a'9e$3/poUܔOtv ˮSk2(rrLYgݓcEY]S6@!^떕ذ `#3yΡ;ζ,:՝+~IN`噳Ǭ[:UkW) k {ӛUUWu'*'Չdl@y(OR4-s͝f#bč*l=Ӳ9y{ɝϏvC<93X+Pٝ0:I4" a~G u:+p;ցZ[FZ) #[ظzzNmӶ)&щ"o=+&lܹ߭GKjN,:wۆa'%:LS#\Wv"Cz:t<A:iu>CF-EOdzn>%-/ m:n0&(=ʇ G5Uc:!fٯƑ#KOsGo^#=.y桍{w_Lo{"3o]>zTu y8,B.>W(?a^y1ÃqjgvuzOqR04K :H'/Y%Z !:08h/h(c4"?g2Leݢ-&~0hU{V\oU{2؊z ^Zt;=!id^e?zkn/ln^B. SiTҏNKv N{mІ,yӟ(!mCF"x,| 2:mQUokiĵFZNw罩o:s\bWwYιdn'7Iy<`Ms9nXwlG@oGT*೏/QQ0*ΌTJn~Q,6m7fXbDpM ,dJ.^3Ø>0\+\XŜ?(Y1Oē+SVu$ h#L˾8~(òQ`~a6*A>4 [ò.!-9"aWr)R{O93ٲ˪+hEQ~*'Ro .FH]SvnQhǏk*L=^Fv<;_XL0بCtًrXcῊST}r0\ox|v0gȎSyכ {?{^<p6'0xӡ/[60S}g{<V ^Z Ç^X`bf0:vaj +?mt0¤@y0S@s Þנ [-?9O_'Gu?[g +dz<D9'GXo1Oh+'0T hp  PowerPoint PresentationSumit Gulwani2142Microsoft PowerPoint@0vc@@ %9GSg  )'    """)))UUUMMMBBB999|PP3f333f3333f3ffffff3f̙3ff333f333333333f33333333f33f3ff3f3f3f3333f33̙33333f333333f3333f3ffffff3f33ff3f3f3f3fff3ffffffffff3ffff̙fff3fffff3fff333f3f3ff3ff33f̙̙3̙ff̙̙̙3f̙3f333f3333f3ffffff3f̙3f3f3f333f3333f3ffffff3f̙3f3ffffffffff!___www4'A x(xKʦ """)))UUUMMMBBB999|PP3f3333f333ff3fffff3f3f̙f3333f3333333333f3333333f3f33ff3f3f3f3333f3333333f3̙33333f333ff3ffffff3f33f3ff3f3f3ffff3fffffffff3fffffff3f̙ffff3ff333f3ff33fff33f3ff̙3f3f3333f333ff3fffff̙̙3̙f̙̙̙3f̙3f3f3333f333ff3fffff3f3f̙3ffffffffff!___wwwünmmsnnmmnJnlml⓻mݼnlmlnmCmgmmnsmsnmDûD⼘sm♒޻ln“JJnݒmmݶmnJnsⒻnmnޑn⓻Jm⍼nnmsݙmnmnmm’՜.+,08    On-screen Show"! .Times New RomanComic Sans MSArial WingdingsSymbolcmsy10SystemNewCenturySchlbkDefault Design1_Default DesignMicrosoft Word PictureMicrosoft Excel Chart/Program Analysis using Random InterpretationProgram Analysis#Design choices in Program AnalysisRandom Interpretation Example 1Example 1: Random Testing#Example 1: Abstract Interpretation!Example 1: Random InterpretationOutline9Linear relationships in programs with linear assignments$Basic idea in random interpretation#Idea #1: The Affine Join operation#Idea #1: The Affine Join operation(Geometric Interpretation of Affine Join Slide 14 Example 2Idea #2: The Adjust Operation#Geometric Interpretation of Adjust$Correctness of Random Interpreter RProof MethodologyOutline Problem: Global value numbering Slide 22+How to execute uninterpreted functions ?Random Linear InterpretationOutlineExample Slide 27 Experiments ExperimentsExperimental measure of errorOutline-Other applications of random interpretation Summary  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles"%_q 0Sumit GulwaniSumit Gulwani  !"#$%&'()*+,-./023456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$-Root EntrydO)Pictures`Current UserSummaryInformation(TPowerPoint Document(1qDocumentSummaryInformation8