ࡱ> `!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˽?T( |  LvPicture Word.Picture.80,Microsoft Word PictureH/ 0|DTimes New Roman0:A 0DComic Sans MSn0:A 0B DArialSans MSn0:A 00Dcmsy10ans MSn0:A 0"@DSymbolans MSn0:A 0 A(.  @n?" dd@  @@`` x#p#h l?   '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$&#38K$ ,$#% 7 *&&&&&&&&'%%0$ %)$^I=B.l\&&&((00""Ja VD2NN$8,+$&%'#AqS"# ('++*'&AH=:2<_J 4?   /X$2$*0Z0;2% 9 0e0e    A A5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| "0e@     @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5%  N E5%  N F   5%    !"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab f@ 57ʚ;,`(ʚ;g4HdHd :A 0Xpp@ <4!d!dL$ 0z<4ddddL$ 0z<4ddddL$ 0zPg4>d>d :A 0vp@ pp2DEFAULTFONTSIZE10.DEFAULTWIDTH3480DEFAULTHEIGHT2729___PPT10 6?  O =)w6A Polynomial-Time Algorithm for Global Value Numbering77$1SAS 2004 Sumit Gulwani George C. Necula2Z2+Global Value NumberingyGoal: Discover equivalent expressions in procedures Applications: Compiler optimizations Copy propagation, Constant propagation, Common sub-expression elimination, Induction variable elimination etc. Program verification Discover loop invariants, verify program assertions Discover equivalent computations across programs Plagiarism detection tools, Translation validation 4o4230 o42 3  mGlobal Value Numbering HNon-trivial Example Existing AlgorithmsVAlgorithms that work on SSA form of the program Alpern, Wegman, Zadeck s (AWZ) algorithm: POPL 1988 Polynomial, Incomplete Ruthing, Knoop, Steffen s (RKS) Algorithm: SAS 1999 Polynomial, Incomplete, Improvement on AWZ Dataflow analysis or Abstract interpretation based Kildall s Algorithm: POPL 1973 Exponential, Complete Our Algorithm: POPL 2004 Polynomial, Complete, Randomized Our Algorithm: this paper Polynomial, CompleteH044+3!0* + + 3   ! t03 J(Why SSA based algorithms are incomplete?  'Abstract Interpretation based algorithm 9OutlineStrong equivalence DAG (SED) The join operation: Idea #1 Pruning an SED: Idea #2 The strongest postcondition operation Fixed point computation xb &'Representing Equivalences )Representing Equivalences pStrong Equivalence DAG (SED)bA data structure for representing equivalences. Nodes n: Type: c, ?, F(n1,n2) Terms(n): set of equivalent expressions Terms() = V Terms() = V [ { c } Terms() = V [ { F(e1,e2) | e1 2 Terms(n1), e2 2 Terms(n2) } 8 variables x, 9 at most one node s.t. x 2 V called Node(x) 41_KC40+*                           Phr SED: ExampleThis SED represents the following partition: Terms(n1) = { a, 2 } Terms(n2) = { b} Terms(n3) = { c, d, F(a,b), F(2,b) } Terms(n4) = { e, F(c,b), F(d,b), F(F(a,b),b), F(F(2,b),b) }\4$4Pg ;OutlineStrong equivalence DAG (SED) The join operation: Idea #1 Pruning an SED: Idea #2 The strongest postcondition operation Fixed point computation &[b &=The Join Operation_G = Join(G1, G2) G is obtained by product construction of G1 and G2 If n= 2 G1 and m= 2 G2, then [n,m]= 2 G Definition of t1 t t2 c t c = c F(l1,r1) t F(l2,r2) = F ([l1,l2],[r1,r2]) t1 t t2 = ?, otherwise Proof of Correctness Terms([n,m]) = Terms(n) Terms(m) (Thus product construction = partition intersection)2}2b2m   -  f ff ff          ?brT. 7?Example: The Join Operation <OutlineStrong equivalence DAG (SED) The join operation: Idea #1 Pruning an SED: Idea #2 The strongest postcondition operation Fixed point computation :;&b &BMotivation: The Prune Operation FThe Prune OperationPrune(G,k) For each node , check if x 2 V is equal to some F-term of size less than k. If not, then delete all the nodes that are reachable from only <   v6 AExample: The Prune Operation :OutlineStrong equivalence DAG (SED) The join operation: Idea #1 Pruning an SED: Idea #2 The strongest postcondition operation Fixed point computation &T%b &>%The Strongest Postcondition Operation  G = SP(G0, x := e) To obtain G from G , do: Delete label x from Node(x) in G0 Let n=<V,t> be the node in G0 s.t. e 2 Terms(n) (Add such a node to G0 if it does not already exists) Add x to V. .RF  :   0PBHD.Example: The Strongest Postcondition Operation   IOutlineStrong equivalence DAG (SED) The join operation: Idea #1 Pruning an SED: Idea #2 The strongest postcondition operation Fixed point computation &{b &G&Fixed Point Computation and ComplexitybThe lattice of sets of equivalences (among uninterpreted function terms) has height at most k. Complexity Dominated by the cost of join operations # of join operations: O(j k) Each join operation: O(k2 N) This requires doing pruning while computing join Total cost: O(k3 N j) k: # of variables N: size of program j: # of join points in programkZgZ1ZZZEZkC1F ,+ rCExample K ConclusionAIdea #1: Join of 2 SEDs = Product construction Idea #2: Prune SEDs (Discovering equivalences among program expressions does not require computing equivalences involving large terms) Future Work Inter-procedural value numbering Abstract interpretation for combined theory of linear arithmetic and uninterpreted functions <  >'  /xP  ` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@x?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>f-K0 *(    6 @  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 `  X*May 15, 2003   0    b"*OSQ Retreat 2003   0    B* ~B  Hp?"@@H  0޽h ? ̙33y___PPT10Y+D=' = @B + Default Design 0 80(    NĤ,e,e P    Z*    NԨ,e,e     \*  d  c $ ?  4  N\,e,e  @  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  T,e,e `P   Z*    T4,e,e `   \*  H  0޽h ? ̙3380___PPT10.47L ( P (    Nad,e,e P   d @*    N|d,e,e    d B*    TTd,e,e `P  d @*    TWd,e,e `  d B*  H  0޽h ? ̙3380___PPT10.47Uip--K0 xp  (   x  c $x  x  c $hy` @   R  s *\; ; \h   s ,,3 A ??0  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B + -K0  $(   r  S @   r  S Pz0  H  0޽h ? ̙33___PPT10i.<+0,+D=' = @B + -K0 m e p   (   x  c $t@     6DS"`?  C x := b a; y := a 3;\0 2 00 <2   6\S"`? p  {c := a b; If (b == 3)H 0 2 00 22  Np ?"6@ NNN?N @ PF Y z := a b;2 0 2  @ H?"0@NNN?N    H?"0@NNN?N [  H ?"6@ NNN?N ,$D 0 qEquivalence problem is undecidable. Simplification Assumptions: Operators are uninterpreted (will not discover x = c) Conditionals are non-deterministic (will not discover y = c) Will discover z = cX@0 21 2$, - n  H ?"0@NNN?Np  j  :True 2  Ht ?"0@NNN?Np (j  ;False 2H  0޽h ?/@       ̙33( J TIMING.|37.1|10.7|5.9|15.|22.6 ___PPT10 . (}H+9pD ' = @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<* @w%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* w%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+M  y-K0 L D   4(   r  S D@     0C"?   !assert(x = y); assert(z = F(y));  "0 2"6  6?"0@NNN?NH   @ 6?"0@NNN?NH X  0j 8   < ?"6@ NNN?N  @ =* 0 2    @ 6?"0@NNN?N Q   6?"0@NNN?N Q   @ 6?"0@NNN?N Q Z   0!C"?  yx := a; y := a; z := F(a);  0 2  0%C"?  yx := b; y := b; z := F(b);  0 2H  0޽h ?_            ̙33___PPT10i.CT+D=' = @B + -K0   $(   r  S <-@   r  S .00  H  0޽h ? ̙33___PPT10i.O+0W;+D=' = @B +$ -K0 ~v  f(   x  c $6@     0 9C"?8  !assert(x = y); assert(z = F(y));  "0 2"6  6?"0@NNN?N888  @ 6?"0@NNN?N088X  0`Z(  <> ?"6@ NNN?N =* 0 2    @ 6?"0@NNN?NAx  6?"0@NNN?NAp  @ 6?"0@NNN?NAJ`~  <,C ?"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  0tO   ,$@ 0 ZAWZ Algorithm: f functions are uninterpreted fails to discover second assertion RKS Algorithm: uses rewrite rules for normalization Does not discover all assertions in little more involved examples. Rewrite rules not applied exhaustively (exp applications o.w.) Rules are pessimistic in handling loops`-#4#4, +  0hZC"?x8 yx := a; y := a; z := F(a);  0 2  0_C"?p 0 yx := b; y := b; z := F(b);  0 2H  0޽h ?_            ̙33N TIMING2|16.4|22.2|12.7|28.5|30.7:___PPT10.CT+IID' = @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<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* '%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* '8%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* -%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* -P%(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* P%(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<* .%(+ p-K0 ! 0 @(   r  S Tk@   n8 @ ! P-    <l @ lG = SP(G0,x := e)>0       <8t  SAssignment Node(0     <x   FG0(0     6}C"?] ( * O x := e* 0 2 `B   0D  `B   0D 0 @8 %   0 P   < %x  `G2= G0>0      <p   UConditional Node (0     < % e  `G1= G0>0      <p   I *0   Z   s *  nf   6+ n | r  BGS|H IS| + k l   <GHI  r    6 u   ;*0 2   <Ț ] : FG0(0  Q8  #  ~p`    <ܟ # G = Join(G10,G20)l0          < 7  SG1040      <譭  Z Join Node4 0   f2   6  T  B c $ _ Z   s *  T   c $F    <г 0  SG2040   H  0޽h ?o             ̙33___PPT10i.++D=' = @B + 0~-K0 d $(  d r d S @   r d S ļ0  H d 0޽h ? ̙33___PPT10i.~+D=' = @B +  J-K0 ` a(   x  c $(ŭ@     0pƭS"`?  na := 1; b := 2; x := F(1,2);60 200 22  B?"0@NNN?N 0 Y  NX̭?"0@NNN?N j  !{ a,1 } { b,2 } { x, F(1,2) }f 20 22  B?"0@NNN?N` H  0޽h ?/@     ̙33___PPT10i./+Ö+D=' = @B +v -K0 um (   x  c $׭@     0حS"`?  na := 1; b := 2; x := F(1,2);60 200 22  B?"0@NNN?N 0   Nޭ?"0@NNN?N j  ;{ a,1 } { b,2 } { x, F(1,2), F(a,2), F(1,b), F(a,b) } f 210 22(1  B?"0@NNN?N`   HX?"0@NNN?N @ h4Such an explicit representation can be exponential. 5 25H  0޽h ?/@     ̙33___PPT10i./+Ö+D=' = @B + PG-K0 $ P(  $ r $ S @    $ S ڭ0<$@ 0  H $ 0޽h ? ̙33 0 TIMING|30.5|37.8 ___PPT10f .&*P+ED: ' = @B D ' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ h%(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' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ R%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$ Rb%(+8 @-K0 f ^ , n (  , x , c $ @    , c $P P0P<$@ 0    , 08S"`?` p  Za, 2:0 2  , 0S"`?  hd,c, F,0 2 , 0S"`?   Lb, ?,0 2 , @ 6?"0@NNN?Nh  , 6?"0@NNN?N , 0S"`?& Le, F,0 2 , @ 6?"0@NNN?N& , 6?"0@NNN?N& , H`?"0@NNN?N0  Jn1, 2  , H,?"0@NNN?NHx h Jn4, 2  , H"?"0@NNN?N80 X Jn3, 2  , H'?"0@NNN?Nh Jn2, 2 H , 0޽h ?O , , ,  , , , , , , , , ,  ̙33b 4 TIMING|5.7|9.3|8.3 ___PPT10 .&*P+ED ' = @B D ' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, -%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, -B%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, BS%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, Sx%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*, x%(+ -K0 l 0(  l x l c $ 4@   x l c $40  H l 0޽h ? ̙33___PPT10i.~+D=' = @B + P-K0 t P(  t r t S L@    t S MPp<$@ 0  H t 0޽h ? ̙33 0 TIMING|43.6|37.1 ___PPT10f .I؉+ED: ' = @B D ' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t %(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t +%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t +`%(+| +-K0 xx 7^ $ v(   x  c $X=@    ! B?"0@NNN?N 0  DG1&( 2  " BB?"0@NNN?N P  DG2&( 2  # H G?"0@NNN?N 0@ CG&( 2 i*8 0  X 0    0KS"`?` Z F:0 2   0+B#style.visibility<*^ %(+ -K0 p 0(  p x p c $h@   x p c $M0  H p 0޽h ? ̙33___PPT10i.~+D=' = @B +; 0.-K0 P H  (   x  c $T@   a  H ?"6@ NNN?NP ,$ 0 w/Discovering equivalences among all expressions ,00 2.  H8 ?"6@ NNN?N@ `,$@ 0 +For the latter, it is sufficient to discover equivalences among all terms of size at most t at each program point (where t = #variables * size of program). Thus, SEDs can be pruned to have a small size."0 2%Z  Hh ?"6@ NNN?Np  ,$ 0 p2Discovering equivalences among program expressions"30 23'  H ?"6@ NNN?Np @ ,$ 0 =vs.0 2  ND?"0@NNN?N [If G=Join(G1,G2), then Size(G) can be Size(G1) Size(G2) There are programs, where size of SEDs after n joins is exponential in n.       N,@%H  0޽h ? ̙33{ . TIMING|20.2|14.= ___PPT10 .I؉+՛DI ' = @B D ' = @BA?%,( < +O%,( < +Ds' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(++0+  ++0+  ++0+  + -K0 `  $(   r  S @   r  S 0  H  0޽h ? ̙33___PPT10i.q`+D=' = @B + 6 n-K0  55 I 3(   x  c $@     H?"0@NNN?N 0@ CG&( 2 s8 9h  I 9h  2  H$?"0@NNN?N` h  > Prune(G,2) 2  4  0(S"`?jH cy2, ?B0 2  5  0P.S"`?9@_ sy1, GR0 2  7  04S"`?0 @~  y4,y5 ?j0 2   C  # 0e0e    BhC DEF 5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||80`<h @   "0e@      @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abYy D  # 0e0e    BC DEF 5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||D0`H0 @   "0e@      @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@Ypy8 P0  H 0P    B<?"0@NNN?N   5G 2 #  08AS"`?0p Z F:0 2 $  0ES"`?@g cy2, FB0 2  %  0 KS"`?@0V sy1, GR0 2  '  08QS"`?h x  y4,y5 ?j0 2   (  0 XS"`? [ F:0 2 ) B H?"0@NNN?NP` *  H?"0@NNN?N` +  0X]S"`?   jy6,?J0 2  ,  0,cS"`?P 0  jy3,?J0 2  -  H?"0@NNN?NPp  . B H?"0@NNN?N@P  /  0liS"`?  jy7,?J0 2  0 B H?"0@NNN?N  1  H?"0@NNN?N  E  # 0e0e    BhC DEF 5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||80`<h @   "0e@      @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abV@v F  # 0e0e    BC DEF 5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||D0`H0 @   "0e@      @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abpVvH  0޽h ?o $ # )  $ ( * # ' - # , . ( + 0 ( / 1  ̙33___PPT10i.+rP+D=' = @B + "-K0 h 0(  h x h c $hs@   x h c $ 3(    > s *dS"`?,$@ 0 f F @ 0 2 x  c $0@   8 u 02  <  u02    s *  8 p2  LG0.0 2    3 BCHDEF(sHX#H@  S" HX   3 BC@DEFG9 s2e@@  S" _Ph !  s *S"`?u 0F _z, u, F<0 2  "  s *lS"`?`  Lx, ?,0 2 $ 0 p  G = SP(G0, u := F(z,x))H0 2  Hl    ;   ,$D 0 3  3 BCHDEF(sHX#H@  S" 9 4  3 BC@DEFG9 s2e@@  S"  5  s *S"`?  \z, F<0 2  6  s *S"`?  Lx, ?,0 2 8 @ B?"0@NNN?N,$@ 0& 9  0e0e    BC0DEF 5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|||00@   "0e@      @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab(,$@ 0# = s *S"`?,$@ 0 o u, F J 0 2H  0޽h ?  5 8  ̙33 6 TIMING|15.8|6.6|5.2___PPT10.$+@+IЀD' = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*; %(D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*8 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*9 %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*> %(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<*= %(+p+0+>  ++0+=  + ]-K0   0(   x  c $@   x  c $"0  H  0޽h ? ̙33___PPT10i.~+D=' = @B + ` -K0 p  P(   r  S T@     S P<$@ 0  H  0޽h ? ̙33jb___PPT10B.u+ED' = @B D ' = @BA?%,( < +O%,( < +D ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* `k%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* k%(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<* 0D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* Dc%(+- ` -K0 ""0 -3 0 !(   x  c $H@     0S"`? @ nx := 1; y := 1; z := F(1,1);60 2 00 22  0S"`? @ nx := 2; y := 2; z := F(2,2);60 2 00 22L  c $@ Q vL  @ c $@g v  0S"`? x $  j u := F(x,y); 0 2 X2  0pL l L  @ c $vN Q L  @ c $ M N `   0S"`?` `  dAssert(u = z); 0 2  0  LL1.0 2   0|  LL2.0 2   0  LL3.0 2   06 0  LL4.0 2 l 0 1 0,$D 0   6@  LG1.0 2    C BCHDEF(sHX#H@  FV   C BC@DEFG9 s2e@@  j>Vl   <0   6 S"`?@@ bz, FB0 2   6S"`?PP ~x,y, 1B0 2l  2 ,$D 0   60 LG2.0 2    C BCHDEF(sHX#H@  L&   C BC@DEFG9 s2e@@  &l   <   6 S"`?P bz, FB0 2   6hS"`?  0  ~x,y, 2B0 2l  3 ,$D 0 !  6$  G3 = Join(G1,G2)n0 2     "  6-6 0  LG3.0 2  #  C BCHDEF(sHX#H@  f v  $  C BC@DEFG9 s2e@@  O^ v  %  H42e  .(  &  64S"`?` `  bz, FB0 2 '  6h9S"`?p p  kx,y,?00 2z ` @ Z )   P:,$D 0( *  0H>` `Z  G4 = Assignment(G3, u := F(x,y))b!0 2   f +  6@ p` ,  0E P  LG4.0 2  -  C BCHDEF(sHX#H@     .  C BC@DEFG9 s2e@@      /  0JS"`?   ~u,z, FB0 2 0  0OS"`?  lx,y, ?00 2H  0޽h ?O          ̙33 B TIMING&|14.|12.6|13.5|18.7B ___PPT10" .$+@+PµD ' = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*1 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*2 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*3 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*) %(+ py-K0   $(   r  S 0\@   r  S ]0  H  0޽h ? ̙33___PPT10i.n+D=' = @B + 0 0 +(   d  c $     s *Þ @    H  0޽h ? ̙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;Ύophr0GTL^| ev0Vi1To Gm'y)9pW@A@#F`džXQmKOh+'0T hp  PowerPoint PresentationoweoweSumit Gulwanise1898 GuMicrosoft PowerPointon@peL@@P%TGSg  )'    """)))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!___wwwnnnmnmnؙnrݒmmnüޒⓑJlCmCDmnmnnnmn⼼mnm⽻mrrݒmnmmnnün“nn⒒mnnmnmnnnⒻlnnⒼݓnsmDnⶼsmmümm“nnn⒒n՜.+,0    cOn-screen Showon-s/{ !Times New RomanComic Sans MSArialcmsy10SymbolDefault DesignMicrosoft Word Picture7A Polynomial-Time Algorithm for Global Value NumberingGlobal Value NumberingGlobal Value NumberingNon-trivial ExampleExisting Algorithms)Why SSA based algorithms are incomplete?(Abstract Interpretation based algorithmOutlineRepresenting EquivalencesRepresenting EquivalencesStrong Equivalence DAG (SED) SED: ExampleOutlineThe Join OperationExample: The Join OperationOutline Motivation: The Prune OperationThe Prune OperationExample: The Prune OperationOutline&The Strongest Postcondition Operation/Example: The Strongest Postcondition OperationOutline'Fixed Point Computation and ComplexityExample Conclusion  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles%_ Sumit GulwaniSumit Gulwani  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)Pictures9Current UserSummaryInformation(TPowerPoint Document(DocumentSummaryInformation8