ࡱ> }z{|n$0iH+*PNG  IHDR?i}gAMA|Q pHYs.#.#x?vIDAThM8`",HhEz# ZВ~6~T~H‡xEg-^P1@S>@ j_󅄈9%ZpTq)P58kO 5e gO$̆M ГM6_GACUِ'2zF>7F< C5z BBC 4AH}* Am/m!F#0x P<Ѐz1T^HBH ?$H߉AyQ,$nDiJ$Tԋ*2CBp‘D5TP UaZZ`E bA-Kxh# PtRP} Ǽo6>E!qH7SCy*QP0ԩ.F VPl0vv-1)7Kˡ~n.-G`[!1^!̄ (!F.C(5[ ZZ*@^dͩ B7 {ZY %,,hif> 4"fjhBA)hQD艸<~`NC+-iH}9A iA#CmS5 >CDO3C=Yz#P!itcMCTA*iCgD-Uz oҹ/S$hTд@3P "bhhr ^ktr A|y-FѐH8@F@ 1sYw!!g/.BPG~^)]@b&Z A~u-P R[ $KJBܛ /ƣ$H^\BA:xY)? Bc^:A`xπDqekhȼ$B=]WG5G!XBڹ%Apz1БQ7G 8B@Ar2V.j Sj5| 񡋗ɉHt<.mh/ҵ>ykF,nwC3,3H g4S*Rs/li] ?>PY%Gcd&" 3GZ 4` #ckJ;NjskOZ;>ȽўU4Ah|ЪB{ꍛPBs&bu<UȽf3B7;5fu}f.Lm@n+9̈́fbݨ/4!7IVZmv%Wؾ!TD  ȉN(Dq-T(?4s_9%I"A>ȝ˱e4;+KDb9 r#s- I(tGBvkA5D8Vi{ "H- N^1FB}t^pQOZnhzBv]Cw,dw653CVgQs= ˆxf+CCqYr݆n?TGk{$;g=㺿:@`#IENDB``!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||>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>@>>~ >(` |   vPicture Word.Picture.80,Microsoft Word PictureN/ 0|DTimes New Roman0z[ 0DComic Sans MSn0z[ 0B DArialSans MSn0z[ 00Dcmsy10ans MSn0z[ 0"@Dmsam10ans MSn0z[ 0" A 0(.2  @n?" dd@  @@`` h ,   '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$$&("3,8-U$1 34689,$#=%> ?@NABC Ob$$0iH+*2$*0Z0;2% 9$r$`[@LȱqDtl@ 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 f@d Oq0ʚ;7,(ʚ;g4dddd z[ 0pp@ <4!d!dL 0z<4ddddL 0z<4ddddL 0zg4>d>d z[ 0vp pr2DEFAULTFONTSIZE100___PPT10 ? ,O =w9Discovering Affine Equalities Using Random Interpretation:9WSumit Gulwani George Necula EECS Department University of California, BerkeleyX%3$Ky)Probabilistically Sound Program Analysis!9Sound program analysis is hard We are used to pay in terms of Loss of completeness or precision Complicated algorithms Long Running Time Can we pay in terms of soundness instead? Judgments are unsound with low probability We can predict and control the probability of error Can gain simplicity and efficiency  K* K *,The Problem of Discovering Affine EqualitiesbDiscover equalities of the form 2y + 3z = 7 Compiler Optimizations Loop Invariants Translation Validation There exist polynomial time deterministic algorithms [Karr 76] involve complicated and expensive operations We present a randomized algorithm as complete as the deterministic algorithms but faster and simpler (almost as simple as an interpreter) t,??-#i,??-#i   "Idea #1: The Affine Join OperationExecute both the branches Combine the values of the variables at joins using the affine join operation w for some randomly chosen w v1 w v2 w v1 + (1-w) v2$0h        ~5Geometric Interpretation of the Affine Join operation66 | Example 2 Idea #2: The Adjust OperationExecute multiple runs of the program in parallel Sample = Collection of states at each program point  Adjust the sample before a conditional (by taking affine joins of the states in the sample) such that Adjustment preserves original relationships Adjustment satisfies the equality in the conditional Use adjusted sample on the true branch6b'b'0Geometric Interpretation of the Adjust Operation11  The Randomized Interpreter R  Completeness and soundness of R We compare the randomized interpreter R with a suitable abstract interpreter A R mimics A with high probability R is as complete as A R is sound with high probability&s9s9}The Abstract Interpreter A Completeness Theorem If T ) g = 0, then S g = 0 Proof: The affine join operation preserves affine relationships And so does the adjust operation %ZZ  Soundness Theorem If T ) g = 0, then with high probability S g = 0 Error probability b: number of branches j: number of joins d: size of the field r: number of points in the sample If j = b = 10, r = 15, d 232, then error probability .4a&% a!Loops and Fixed Point ComputationVThe lattice of sets of affine relationships has finite depth n. Thus, the abstract interpreter A converges to a fixed point. Thus, the randomized interpreter R also converges (probabilistically) We can detect convergence by comparing the ranks of the samples in two successive iterations rank = number of linearly independent relationships 6"4"4 Related WorkAbstract interpretation on sets of affine relationships [Karr76, Cousot77] Operations are comparatively complicated and expensive Value numbering More of syntactic flavor than semantic Random testing Can exhibit counterexamples but doesn t prove assertions Equivalence testing for read-once branching programs Similar idea of affine joins KZ7ZZ'ZZ9Z7ZZZZK7'97  Conclusion and Future WorkRandomization can help achieve simplicity and efficiency at the expense of making soundness probabilistic Interesting possible extensions: Memory Non-Linear assignments Inequalities Dependent conditionalsFj!Bk!B/x<  ` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@x?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>fK0 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 @(    N ut;ut; +   x*  Y,,YY  Nut;ut;  +  z*  Y,,YYd  c $ ?  4  Nut;ut;  \T  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  T0&ut;ut; 5`   x*  Y,,YY  T&ut;ut; 5 `  z*  Y,,YYH  0m  ? ̙3380___PPT10.47L P 0(    N8ut;ut; +   ^*  Y,,YY  NXut;ut;  +  `*  Y,,YY  Tut;ut; 5`   ^*  Y,,YY  T4ut;ut; 5 `  `*  Y,,YYH  0m  ? ̙3380___PPT10.47UifK0 xp  (   x  c $z  z x  c $z`   z R  s *\; ; \h   s ,,3 A ??0  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B + fK0 @ $(   r  S T@   r  S 70  H  0޽h ? ̙33___PPT10i.v+D=' = @B + fK0  0(   x  c $e@   x  c $f00  H  0޽h ? ̙33___PPT10i.v+D=' = @B +" + (     0lC"? Ka := 0; b := 1; 0 2  00uC"?  Ka := 1; b := 0; 0 2  0xC"? p  n2c := b  a; d := 1  2b; 0 2  0|C"?P P b&assert (c + d = 0); assert (c = a + 1) '0 2'  0@*C"?   0c := 2a + b; d := b  2;60 2F  S 7WF  @ S YWL  @ c $?HX2  0 ;k F  @ S  d L  @ c $ HSPRB  s *DpRR  0xp  =T 0 2  0p  =T 0 2  0xp =F 0 2  0    =F 0 2R2  s *P0`F  S  B X  0?d  <GHW-I^  6G޼HI޼X  00 d  <GHfI ^  6GHI  # 6 @  Example 1 $ 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 % H< ?"6@ NNN?N@ `&  Random testing will have to exercise all the 4 paths to verify the assertions Our algorithm is similar to random testing However, we execute the program once, in a way that it captures the  effect of all the paths 2z  p00 )  `@ P,$D 0B * HDjJ?"0@NNN?N p0B +  HDjJ?"0@NNN?N p00H  0޽h ?@                              33___PPT10."(+EAWD~' = @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<*$ %(+ fK0 `  (   x  c $Ȗ@     c $Ж   " 0Pp  0C"? `  Ka := 2; b := 3; 0 2  0C"?   Ka := 4; b := 1; 0 2  6 Pz    a = 2 7 4 = -10 b = 3 7 1 = 15n!0   F  S    F  @ S  9  R2  s *  @ 0   <Nz ?"6@ NNN?N Pz E(w = 7)"0 2  H  0޽h ?/@    ̙33___PPT10i.v+D=' = @B +1 &#$ n(     0˖C"? Ka := 0; b := 1; 0 2  0hWzC"?  Ka := 1; b := 0; 0 2  0C"? p  n2c := b  a; d := 1  2b; 0 2  0HC"?P P b&assert (c + d = 0); assert (c = a + 1) '0 2'  60 @,$D 0 G a = -4, b = 50   6` ,$D 0 da = -4, b = 5 c = -39, d = 39 *0    0xC"?   0c := 2a + b; d := b  2;60 2   6`v ,$D 0 F a = 1, b = 0 0     6#`P ,$@ 0 F a = 0, b = 1 0     6|'0  ,$D 0 Ua = -4, b = 5 c = -3, d = 30 F   S 7WF   @ S YWL  @ c $?HX2  0 ;k F  @ S  d L  @ c $ HSPRB  s *DpRR  6p-0  ,$@ 0 Va = -4, b = 5 c = 9, d = -90   01p  =T 0 2  0X5p  =T 0 2  08p =F 0 2  0@<   =F 0 2R2  s *P0`F  S  B X  0?d  <GHW-I^  6G޼HI޼X  00 d  <GHfI ^  6GHI    0|A&,  \w1 = 5:0 2  ! 0 G&  ,$ 0 ]w2 = -3:0 2  " 6K @  Example 1 $ HM ?"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.  2H  0޽h ?@                                 331)___PPT10 ."(+DU' = @B D' = @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<* %(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%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ 5o%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ o%(++0+  ++0+  ++0+   ++0+   ++0+   ++0+  ++0+!  +/ fK0 T (   x  c $l@   B  0Do n> ,$@ 0XB  0Do ^ XB  0Do`  $ <4o .   ;x0  % 0r ;y0 LB ) c $D ' '  4 6W-v ,$ 0 C x + y = 1 0   5 0z0 @ ,$  0 ?x = 20 B 7 NDo?"0@NNN?N`$ $ ,$@  0 8 0~   H(x = 0, y = 1)0  9 0̂ z  H(x = 1, y = 0)0  ; Hx ?"6@ NNN?N'pG .( 2L < Hp ?"6@ NNN?N @,$D 0 b.: State before the join : State after the join/ 2/{ > Hd ?"6@ NNN?N` L ,$@ 0  satisfies all the affine relationships that are satisfied by both (e.g. x + y = 1, z = 0) Given any relationship that is not satisfied by any of (e.g. x=2), also does not satisfy it with high probability xi 2 2 2i [  K  fXgֳgֳ3?"6@ NNN?N0, 6"0( 2   L Zgֳgֳ3?"6@ NNN?N nz  M Zgֳgֳ3?"6@ NNN?NZ   N Zgֳgֳ?"6@ NNN?N (:,$@ 0 O Zgֳgֳ?"6@ NNN?N8,$@ 0 P Zgֳgֳ?"6@ NNN?N V r,$D  0> R  fDgֳgֳ3?"6@ NNN?Nb(,$@ 0 6"0( 2  > S  fФgֳgֳ3?"6@ NNN?N` 0 ,$D 0 6"0( 2   T Zgֳgֳ?"6@ NNN?N` @ ,$@  0H  0޽h ? ̙33JB___PPT10".v+QD' = @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<*4 %(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*N %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*O %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*< /%(DY' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*> i%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*R %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P %(D~' =%(D&' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*5 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*7 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*> j%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*T %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*S %(++0+4  ++0+5  ++0+R  ++0+S  + fK0   !  (   x  c $@     0HC"?P F a := x + y 0 2   0ƲC"? P  Q b := a, 0 2  0˲C"? P  eb := 2x 0 2  0lβC"?0@ Kassert (b = 2x) 0 2X2  0 @ L  c $@   0Ҳ  =T 0 2  0ֲ  =F 0 2RB  s *DL  c $@  <ٲ@,$D 0 F If (x = y) 0  d  <GHjtI ^  6G LHI L F  @ S   F  S  ( s ! H߲ ?"6@ NNN?N p e,$@ 0 SIdea #1 is not enough We need to make use of the conditional x=y on the true branchT 2TH  0޽h ?o                   ̙33^V___PPT106.v+ ~D ' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*! %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*! T%(+ fK0  $(   r  S z@  z r  S z00 z H  0޽h ? ̙33___PPT10i. +D=' = @B +=E fK0 M Z(   x  c $@   ~  @ Hgֳgֳ?"r  Zgֳgֳ?"6@ NNN?Np@ ,$@ 0  Zgֳgֳ3?"6@ NNN?NP   Zgֳgֳ3?"6@ NNN?N@  Zgֳgֳ3?"6@ NNN?N,F  Zgֳgֳ?"6@ NNN?N  ,$@ 0  Zgֳgֳ?"6@ NNN?N  @ ,$@ 0  Zgֳgֳ?"6@ NNN?N| @ ,$D 0  Zgֳgֳ3?"6@ NNN?NP    Zgֳgֳ?"6@ NNN?N 2 ,$D  0B  TDo?"0@NNN?NPp ,$@ 0B + ZDo?"0@NNN?N` ^ ,$@ 0 2 Bp ?"6@ NNN?N` 0 BOriginal Point 2C 3 B@ ?"6@ NNN?N  ,$ 0 _Conditional (e2=0)0( 2 ( 4 B ?"6@ NNN?N  ,$ 0 DAdjusted Point( 2B 5 @ ZDo?"0@NNN?N 8B 6 ZDo?"0@NNN?N  ,$D 0B 8 6D?"0@NNN?N  B > <Do?"0@NNN?NPpp ,$@  0B ? BDo?"0@NNN?N pp ,$@  0B @ <Do?"0@NNN?N pp,$@ 0B A @ <Do?"0@NNN?N  ,$D 0B B @ BDo?"0@NNN?N H ,$@ 0B C @ <Do?"0@NNN?N p` ,$@ 0B G BDo?"0@NNN?N P ,$@  0B H <Do?"0@NNN?N Ph ,$@  0B K <Do?"0@NNN?N p,$@ 0< L B ?"6@ NNN?NP `p,$ 0 X(lies on e1=0). 2  q M B8 ?"6@ NNN?N p  ,$ 0 (lies on e1=0 e2=0)\( 2   H  0޽h ?   ̙33((___PPT10(.v+VDgDo'' = @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<*3 %(D' =%(D' =%(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<*4 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*6 %(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*K %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*G %(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<*@ %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*B %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*C %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*A %(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*+ %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*M %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*L %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*M %(++0+3  ++0+4  ++0+L  ++0+M  ++0+M  + fK0 7/ (   x  c $D@     0FC"?{ @x := e0 2RB  s *D{  6HJ ES(0    6tG+0 HS (0  RB  s *D  6Qp ?e = 0 ?0   0XUjd @True 0 2  0YpMPj AFalse 0 2X  0sUpPd  <G@HI@bU ^  6G]H*I]bp   6]z@ HS (0    6bP P FS1(0    6xg5` FS2(0  X2  00T `F  @ S 9} 7L  c $`l p F  S *[ 7  6 n p FS1(0    6p0 p FS2(0    6t `  ES(0  x  0yC"? ` ,$@ 0 2S1 = Adjust(S ,e) S2 = S T0 2      0C"? pp ,$D 0  Si = S1i wi S2i0 2              ,B  HD?"0@NNN?NJjB  BD?"0@NNN?N@  0|C"?  ,$ 0 Si = S i[x e]l0 2  $B  BD?"0@NNN?N@``H  0޽h ?_         ̙33  ___PPT10 .v+ DS ' = @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<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(+8+0+  + fK0 $ $(  $ r $ S @   r $ S `0  H $ 0޽h ? ̙33___PPT10i.3+D=' = @B +b fK0  7 (   x  c $@     6쥶 ~ ?e = 0 ?0   0̬0 @True 0 2  0 AFalse 0 2X  0pd  <G@HI@* ^  6G]H*I]`*   6H ` HT (0    6p  FT1(0    6轶U@0  FT2(0  X2  0 - ] PF  @ S )V 'L ! c $PE I F " S 4 ' ( 6¶i ` FT1(0   ) 6ȶ ` FT2(0   * 6hͶi 9 p ET(0  r + 0ѶC"?  ,$@ 0 6T1 = T [ { e = 0 } T2 = T l0 2             , 0ٶC"? P` ,$D 0 +T = { g=0 | T1 ) g=0, T2 ) g=0 } ,0 2   B - HD?"0@NNN?NjB . BD?"0@NNN?N PP 0 0C"? `Y ,$ 0 JT = T [x /x] [ { x = e[x /x] }8&0 2, 1 BL?"6@ NNN?N b.Abstract Domain = Sets of affine relationships/ 2/ 2 0TXC"? @x := e0 2RB 3 s *D 4 6 ET(0   5 6KP  HT (0  RB 6 s *D; B 7 BD?"0@NNN?N ``H  0޽h ?_     "   !  ̙33  ___PPT10 .v+WDS ' = @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<*+ %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, ,%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(+8+0+0  + fK0  ( 0(  ( x ( c $@   x ( c $l00  H ( 0޽h ? ̙33___PPT10i.v+D=' = @B + fK0 * " 0,  (  , x , c $ @    , c $00<$@ 0  B , HDjJ?"0@NNN?N\,$@  0B , HDjJ?"0@NNN?Nd,$D  0l , jA ?txp_fig"6@ NNN?N70 $@  0` SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $$(2d)^b\left(\frac{j+1}{d}\right)^r$$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False*RESOLUTION300"TIMEOUT156BITMAPFORMATbmpmono8 DEBUGINTERACTIVETrue(ORIGWIDTH1388PICTUREFILESIZE 13526 ,  pA ?txp_fig"6@ NNN?N/ a P<4 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&ORIGWIDTH906PICTUREFILESIZE2062H , 0޽h ? ̙33.&___PPT10.v+>.CD' = @B D' = @BA?%,( < +O%,( < +D' =%(%(DT' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, 4%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, 6L%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, Lb%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, bu%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, u%(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' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, %(+ fK0 0 0(   x  c $'@   x  c $t(0  H  0޽h ? ̙33___PPT10i.v+D=' = @B + fK0  0(   x  c $0@   x  c $10  H  0޽h ? ̙33___PPT10i.v+D=' = @B + fK0 @ 0(   x  c $C@   x  c $|D0  H  0޽h ? ̙33___PPT10i.v+D=' = @B + 0 0 +(   d  c $     s *< \T    H  0m  ? ̙33x\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>G|Ov@K3ThW|0e_D0mAZ\pW}b? 2Oh+'0T hp  PowerPoint Presentationoweowegulwani785Microsoft PowerPointon@\[@@ يFGSg  )'    """)))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!___wwwssⒶr޼mmöޑޒmrüⒶõ’lgJmCJrmmmÒsm޼n¶rݙÓrÒm⶘Òmmn޼smsݒõmrݶmsÒm¼s’ݙssrsݼ޵lûsssmsnünnݙrsޒs՜.+,0t    On-screen Shown-sF{A Times New RomanComic Sans MSArialcmsy10msam10Default DesignMicrosoft Word Picture:Discovering Affine Equalities Using Random Interpretation*Probabilistically Sound Program Analysis!-The Problem of Discovering Affine EqualitiesSlide 4#Idea #1: The Affine Join OperationSlide 66Geometric Interpretation of the Affine Join operation Example 2Idea #2: The Adjust Operation1Geometric Interpretation of the Adjust OperationThe Randomized Interpreter R! Completeness and soundness of RThe Abstract Interpreter ACompleteness TheoremSoundness Theorem"Loops and Fixed Point Computation Related WorkConclusion and Future Work  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles_2gulwanigulwani  !"#$&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghiklmnopqstuvwxy~Root EntrydO)PicturesHCurrent UserrSummaryInformation(?TPowerPoint Document(%2DocumentSummaryInformation8j