ࡱ> n6 O[6Ҕn݁·[_PNG  IHDR 4 pHYs/tEXtSoftwareAFPL Ghostscript 8.00< IDATxK8IEm,Q5(,Y`zQ!,+õ@/%1^[PHC+IAK+lܳS:@ƨ*̅[!{4($NOǮ !Wp$:!"oCdx;.qzR ꌨw{$s /$BJq$(I;hhLAݹ,.K 9/ jez-Ukg@Sm ,@V"dL\,!HfQ j ^` d &,Ꙛl KYsZB&.=9(D+UK"IKleIw@z!B&" 9քL,V~BȦ#\z-%\1xc ֪Z-d1u,?҇H8@)X<!֫qR2ƭLgDW">db 9l6M@!mD oId=1c&ebex$ 9}$R&"Ϟ>9l(ĚbD6u\R&&=-^=BDգDn() ٯs1u&e!U.alC217ƐrR&&WlML D=0tW'eb WCTՉTi B&&=Q=*%];)+@t?2ѐM?AAIhȪ^,N廴LtHz:ATLtP/?i1Z&"T%zA&S~d!KL!yiL]ZsF&ʡv}茫h(Ȗ|CAYLdMny߬)vBfdғ vsRUN@F& "`T<+#9wt&5|ddrAf~]VJOu6 $YӛNHWb^A%++²3<Ʈk;>z#{$<ԜٶgYWTY3jgCF&'$c] wjfd,D0 $g譏$אeҤBHCQ!%4S Wᶥjq9cQmUI})3ʒ5!025Bwu蚪MY>:iwn+u4,Gjֶ)`z϶'ȶ`65фlY=!_C ^Rۙ\- K@"^>=~L@gdQ1h4y4 +7[A! 3뉗驿EXObJ@λdZx> >5\!ð^<~`+Fh fa:wA.nS*IC.sB1 BBˬ9̺ÜDVOH @ׇD[ hb7w Z!P( ؎銾J(eA@1(XȄ`܊BvPB7`>i4J(ds ' ![JW[|Q b=7C B!p̈́XSvC {9!@ԆJ!;›[cĵ Y P"]*…"#Ȥ!O|O  Bt`\(1dA. EA6 Ł >X5d wB!gT(2GB!` Z@.[y'jRxT(eloT(!dG ߡ0.0\B"_P3VC5 cB!,V@A$ӐĮǃ(J@Pk! B P" bl| ʆCFQl AL:>9l*\@ⒸMOM`l 5mx?KZ(n g z3 M#]BV9o{eVA>e2A>- X;3!,1@Z(`nHצG=lB(`넘%>oMW9fbu|=4$'ߖӇ=qt^ J,!Į`P5}fɮ%^N 昮l4;-Jz$<r'-,M 2?{DG/@n-/?40Y)ЇNkTqOurU! aC0! aC0! aC0! aC0! aC0! aC0! aCG@! aC^edC0! aC0! aC0! aC0! aC0! aC|gHꧡ^uB_}%WB&" D0;\!56C ~@ 㮟Yod .0C"o ).&Đ+n )-]kҐ4Ajw4'Mx! I6~S  @HM]Cj S?s d Kgo3/%gH_HKPϐ!}!-A=CBtto n )--'MjBZVOZ BZVOZ BZVOZ B BBat4 i o3'-fHOH[! .ޮ'3!6 do.x}X:!bzY5e@jȬ.C{ S?IOΐ!up#dR7>~gHXoݔjr" r+!SGTr R)6 YDTM: OT@ڕ{>QcgtZf ٯ[8Ǚișb"xޅ'dk!  V{9t}h{.+;W?2|?(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˽U( |  2vPicture Word.Picture.80,Microsoft Word Picture/ 00DTimes New Roman0:A 0DComic Sans MSn0:A 0B DArialSans MSn0:A 0"0Dcmsy10ans MSn0:A 0" A9.Z  @n?" dd@  @@``   H1   '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$&#38K$ 49g$#% 7 *&&&&&&&&'%%0$ %)$i^I=mDn.l\&&&((A0 /DC%~A$# $$05<KFdPS1/Xb$O[6Ҕn݁·[_> 2$*0Z0;2% 9>  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 @ Oq0ʚ;7,(ʚ;g4BdBd :A 0pp@ <4!d!dL$ 0l{<4ddddL$ 0l{<4ddddL$ 0l{g4>d>d :A 0vp@ pp2DEFAULTFONTSIZE10.DEFAULTWIDTH3480DEFAULTHEIGHT2009___PPT10 6?$,08/28/04O =#.wJPath-Sensitive Analysis for Linear Arithmetic and Uninterpreted FunctionsKJ3  aSAS 2004 Sumit Gulwani George Necula EECS Department University of California, BerkeleybZ/3N  O  P  _OutlinevExisting approach (MVR) vs. our approach (FCED) FCEDs for linear arithmetic FCEDs for uninterpreted function terms40F0G>2 K    `OutlinewExisting approach (MVR) vs. our approach (FCEDs) FCEDs for linear arithmetic FCEDs for uninterpreted function terms<1F3)P* ZProblem Definition4e = q | y | e1 e2 | q e | if b then e1 else e2 b = c | b1 b2 | b1 b2 e: conditional linear arithmetic expression b: boolean formula y: rational variable c: boolean variable q: rational constant Construct FCED for an expression e, given FCEDs for its subexpressions. Check 2 FCEDs for equivalence.322~I2         ~hb~!J  [FCEDAn FCED f is a DAG with the following kind of nodes. f := y | q | Plus(f1,f2) | Minus(f1,f2) | Times(q,f) | Choose(f1,f2) | Guard(g,f) Choose(f1,f2) means f1 or f2 Guard(g,f) means if g then f Boolean expressions g are represented using ROBDDs g := true | false | c | If(c,g1,g2) b52R2:2Z6          4   P`   B'@Example cExample \FCED ConstructionFCED(y) = Leaf(y) FCED(q) = Leaf(q) FCED(e1+e2) = Plus (FCED(e1), FCED(e2)) FCED(q e) = Times(q,FCED(e)) FCED(if b then e1 else e2) = Choose(Guard(R(b),e1), Guard(R(NOT(b)),e2) b/VG ~,G^FCED ConstructionFCED(y) = Leaf(y) FCED(q) = Leaf(q) FCED(e1+e2) = Plus (FCED(e1), FCED(e2)) FCED(q e) = Times(q,FCED(e)) FCED(if b then e1 else e2) = Choose(||R(b),FCED(e1)||, ||NOT R(b), FCED(e2)||) :6Vz,HANormalize Guard Operator Y!Example: Normalize Guard Operator <(Randomized Equivalence Testing for FCEDs#0Assign hash values to nodes of FCEDs in bottom-up manner V: FCED Node ! Integer V(Leaf(q)) = q V(Leaf(y)) = ry V(Plus(f1,f2)) = V(f1) + V(f2) V(Choose(f1,f2)) = V(f1) + V(f2) V(Guard(g,f)) = H(g) V(f) H: Guard ! Integer H(true) = 1, H(false) = 0 H(c) = rc H(If(c,g1,g2)) = rc H(g1) + (1-rc) H(g2)QZ|ZZQZG&  + -A X)Randomized Equivalence Testing for FCEDs # Completeness f1 f2 ) V(f1) = V(f2) Soundness f1 f2 ) Pr[V(f1) = V(f2)] s/t s: maximum # of nodes in a FCED t: size of set from which random values are chosen Proof: 9 1-1 Poly: FCED ! Polynomials such that V(f) is the value of Poly(f)$Za4>PaOutlinewExisting approach (MVR) vs. our approach (FCEDs) FCEDs for linear arithmetic FCEDs for uninterpreted function terms41FQ'P* ]Problem Definition e = y | F(e1,e2) | if b then e1 else e2 b = c | b1 b2 | b1 b2 e: conditional uninterpreted function term b: boolean formula y: variable c: boolean variable Construct FCED for an expression e, given FCEDs for its subexpressions. Check 2 FCEDs for equivalence(22_I2         _htS 5  bFCEDAn FCED f is a DAG with the following kind of nodes. f := y | F(f1,f2) | Choose(f1,f2) | Guard(g,f) Choose(f1,f2) means f1 or f2 Guard(g,f) means if g then f Boolean expressions g are represented using ROBDDs g := true | false | c | If(c,g1,g2) 52/2:2Z6       4   >Z  B'TFCED ConstructionFCED(y) = Leaf(y) FCED(F(e1,e2)) = F(FCED(e1), FCED(e2)) FCED(if b then e1 else e2) = Choose(||R(b),FCED(e1)||, ||NOT R(b), FCED(e2)||)   H+6U'Randomized Equivalence Testing of FCEDs"Assign hash values to nodes of FCEDs in bottom-up manner V: FCED Node ! Tuple of k integers K depth of any FCED V(y) = [ry,& ry] V(Choose(f1,f2)) = V(f1) + V(f2) V(Guard(g,f)) = H(g) V(f) V(F(f1,f2)) = V(f1) M + V(f2) N M, N: random k k matrices JssG   %&# ES)Randomized Equivalence Testing for FCEDs #Completeness f1 f2 ) V(f1) = V(f2) Soundness f1 f2 ) Pr[V(f1) = V(f2)] s: maximum # of nodes in a FCED t: size of set from which random values are chosen Proof: more involvedkConclusion and Future Work]Randomization can help achieve simplicity and efficiency at the expense of making soundness probabilistic. Integrate randomized techniques with symbolic algorithms Few interesting possible extensions: Combination of uninterpreted functions with arithmetic Partially interpreted functions like commutative and/or associative functions Model memoryFl_m_/xP<  ` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@x?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>f-K0 bZ(    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  0d `  @*   0    B*   0     B* ~B  Hp?"@@H  0޽h ? ̙33 Default Design 0 80(    N4,e,e P    Z*    N8,e,e     \*  d  c $ ?  4  Nh=,e,e  @  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  TA,e,e `P   Z*    TF,e,e `   \*  H  0޽h ? ̙3380___PPT10.47L ( P (    NK,e,e P    @*    N,e,e     B*    TO,e,e `P   @*    TV,e,e `   B*  H  0޽h ? ̙3380___PPT10.47Ui3-K0 xp  (   x  c $L   x  c $ 0`    R  s *\; ; \h   s ,,3 A ??  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B +0|-K0 , (  ,  , 08`C"? by := 2; z := a;6 0 200 22 , 0xC"?O+ by := a; z := 2;6 0 200 22 , 0@cC"?   du := 1; v := 1+a;6 0 2 00 22; , 0lC"?M M t1 := y-u; t2 := v-z;T0 2    , F , S "rF , @ S L , c $@X2  , 0~ } F  , @ S   L  , @ c $ M RB  , s *Dptt`  , 0h0* @True 0 2 , 0  @True 0 2 , 0&p  AFalse 0 2 , 0@  AFalse 0 2R2 , s *}kF , S  d  , <ܠ`- @( 2  d , <GN HVIN "-^ , 6G0hH`I0hX , 0@? d , <G-HI-d? ^ , 6GhHIh  , 6 @ Example , 0$C"?   du := a-1; v := 3;6 0 200 22J , 0C"? 0  Assert(t1=t2 t1=1 z=2); 0 2    , 6?"0@NNN?NM  , H, ?"6@ NNN?N@`  Qa=2? 0 2  , H ?"6@ NNN?N0  JAll 3 asserts are true 2 , H ?"6@ NNN?Nr Ha=2?( 2 H , 0޽h ?`, , , , , , , , , , , , , , ,  , , , , , , , , ,  , , ,  , , ,  , , ,  33___PPT10i."(+D=' = @B +z(`-K0 z r ##0 (  0  0 00ƢC"? by := 2; z := a;6 0 200 22 0 0̢C"?O+ by := a; z := 2;6 0 200 22 0 08ѢC"?   du := 1; v := 1+a;6 0 2 00 22; 0 0L֢C"?M M t1 := y-u; t2 := v-z;T0 2    , F 0 S "rF 0 @ S L 0 c $@X2  0 0~ } F  0 @ S   L  0 @ c $ M RB  0 s *Dptt`  0 0Hߢ0* @True 0 2 0 0  @True 0 2 0 0&p  AFalse 0 2 0 0$  AFalse 0 2R2 0 s *}kF 0 S  d  0 <t`- @( 2  d 0 <GN HVIN "-^ 0 6G0hH`I0hX 0 0@? d 0 <G-HI-d? ^ 0 6GhHIh  0 6x @ -Path-Insensitive Analysis 0 0@C"?   du := a-1; v := 3;6 0 200 22J 0 0C"? 0  Assert(t1=t2 t1=1 z=2); 0 2    0 6?"0@NNN?NM  0 HX  ?"6@ NNN?N,<  C*& 2  0 H ?"6@ NNN?N0 ,$D 0 ZMost PTIME analyses treat conditionals as non-deterministic. They will verify only t1=t2 F[ 2T   0 H ?"6@ NNN?N' E*( 2   0 s 0e0e    BbC,DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| db~b[?ddH Zw w,@s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abf7,$D 0z  p00 !0  0P ,$@ 0B "0 HD1?"0@NNN?N p0B #0  HD1?"0@NNN?N p00H 0 0޽h ?`0 0 0 0 0 0 0 0 0 0 0 0 0 0 0  0 0 0 0 0 0 0 0 0  0 0 0  0 0 0  0 0 0  33* TIMING|6.7|9.V___PPT106."(+m`D ' = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*!0 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0 =Y%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* 0 %(+0-K0 !!0##4 (  4  4 0 C"? by := 2; z := a;6 0 200 22 4 0l&C"?O+ by := a; z := 2;6 0 200 22 4 0+C"?   du := 1; v := 1+a;6 0 2 00 22; 4 00C"?M M t1 := y-u; t2 := v-z;T0 2    , F 4 S "rF 4 @ S L 4 c $@X2  4 0~ } F  4 @ S   L  4 @ c $ M RB  4 s *Dptt`  4 0h:0* @True 0 2 4 0>  @True 0 2 4 0A&p  AFalse 0 2 4 0E  AFalse 0 2R2 4 s *}kF 4 S  d  4 <P`- @( 2  d 4 <GN HVIN "-^ 4 6G0hH`I0hX 4 0@? d 4 <G-HI-d? ^ 4 6GhHIh  4 6pT @ +Path-Sensitive Analysis 4 08VC"?   du := a-1; v := 3;6 0 200 22J 4 0 \C"? 0  Assert(t1=t2 t1=1 z=2); 0 2    4 6?"0@NNN?NM  4 HTf ?"6@ NNN?NIV  Rc14 2   4 Hk ?"6@ NNN?N  ,$@ 0 We can do better by doing a boolean abstraction of conditionals. Each atomic predicate is abstracted to a boolean variable This will also verify t1=1 This is still abstract though! z=2 not verified undecidable to reason completelyA 2; 2: 22 2A; "2>HU  4 Hy ?"6@ NNN?Niv Fc1( 2 z  p00  4  ur,$D 0B !4 HDjJ?"0@NNN?N p0B "4  HDjJ?"0@NNN?N p00 #4 s 0e0e    BC,DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| ~cHRZI ,@s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abf,$D 0H 4 0޽h ?`4 4 4 4 4 4 4 4 4 4 4 4 4 4 4  4 4 4 4 4 4 4 4 4  4 4 4  4 4 4  4 4 4  33___PPT10."(+~TD' = @B DU' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* 4 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*#4 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*#4 %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4 %(+ f-K0 p $(   r  S d2@   r  S 0  H  0޽h ? ̙33___PPT10i.،wD}+D=' = @B +I-K0 L:D:@@ 47(     0C"? by := 2; z := a;6 0 200 22  0䍮C"?N* by := a; z := 2;6 0 200 22  0hC"?   du := 1; v := 1+a;6 0 2 00 22;  0dC"?M M t1 := y-u; t2 := v-z;T0 2    , F  S !F  @ S L  c $^X2  0~  F  @ S   L  c $ M RB  s *D  0* @True 0 2  0V*P @True 0 2  0V IP AFalse 0 2  0*X AFalse 0 2R2  s *|F  S  c X  0*d  <GhHIhI!^  6GH6II*X  0^3l d  <GxHIxc ^  6G|HKI|3   6 @ bMulti-Valued ROBDDs (MVRs),   s 0e0e    BSC DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| US~SSe\$$n n @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abEn,$D 0z  p00   0| ,$D 0B  HD1?"0@NNN?N p0B   HD1?"0@NNN?N p00l   @  ,$D 0   Hܷ ?"6@ NNN?N L  >c1 0 2     <$?"0@NNN?N `  ?2"0( 2     <T?"0@NNN?N `  ?a"0( 2   ! B 6?"0@NNN?N  ` "  6?"0@NNN?N i `6 #  H ?"6@ NNN?NR  xy =X0 2      l   ?  ,$D 0 $  H8ɮ ?"6@ NNN?N  >c2 0 2   %  <ͮ?"0@NNN?N$ `  ?1"0( 2   &  <pЮ?"0@NNN?N*` Aa-1"0( 2   ' B 6?"0@NNN?N @` (  6?"0@NNN?N@ `6 )  HtԮ ?"6@ NNN?N   xu =X0 2       * 0ڮC"?   du := a-1; v := 3;6 0 200 22& + 0߮C"?   Assert(t1=t2); Assert(t1=1);n0 2     , @ 6?"0@NNN?NM  - H ?"6@ NNN?NH Bc1$ 2  . HD ?"6@ NNN?N%QE  Bc2$ 2 ) / H  ?"6@ NNN?NX ,$ 0 ?q|MVR(t1)| = |MVR(y)| |MVR(u)| MVR(t1) does not share nodes with MVR(y) and MVR(u) Need a normal form for leavesZr 2  LP % l l hP > hP,$D 0 0  HD ?"6@ NNN?N >c1 0 2   1  H ?"6@ NNN?NS >c2 0 2   2  H( ?"6@ NNN?N? >c2 0 2   3 B 6?"0@NNN?N# 4  6?"0@NNN?N# 5  <?"0@NNN?Nh`X =1 0 2   6  <,?"0@NNN?N|` @-a+3 0 2   7  <?"0@NNN?Nw`0 ?a-1 0 2   8  <?"0@NNN?NA`P =1 0 2   9 B 6?"0@NNN?N` :  6?"0@NNN?N` ; B 6?"0@NNN?NT` <  6?"0@NNN?N`7 =  HX ?"6@ NNN?N yt1 =X0 2      H  0޽h ?_           *               *     !   "  $ % ' $ & (  + , 0 1 3 0 2 4 1 5 9 1 6 : 2 7 ; 2 8 <  337( TIMING |250.2___PPT10."(+D{' = @B D6' = @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<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ %(D4' =%(D' =%(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+/  +;-K0 //3f #-(     0yC"? by := 2; z := a;6 0 200 22  0C"?R. by := a; z := 2;6 0 200 22  0C"?   du := 1; v := 1+a;6 0 2 00 22;  08C"?M M t1 := y-u; t2 := v-z;T0 2    , F  S %F  @ S L  c $^X2  0~  F  @ S   L  c $ M RB  s *D  0ȑ.  @True 0 2  0V. P @True 0 2  0V MP AFalse 0 2  0.\ AFalse 0 2R2  s *F  S  g X  0.d  <GhHIhI%^  6GH6II.X  0^7l d  <GxHIxg ^  6G|HKI|7  # 6 @ b,Free Conditional Expression Diagrams (FCEDs)& $ s 0e0e    BSC DE(F0 @  Ԕ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| US~SSe\$$n n @s " 0e@        @ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN 5%  N 5%  N    5%    !"?N@ABC DEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abInF  p00 )  0 B * HD1?"0@NNN?N p0B +  HD1?"0@NNN?N p00 , H ?"6@ NNN?N L  >c1 0 2   - <?"0@NNN?N`  ?2"0( 2   . <4?"0@NNN?N`  ?a"0( 2   / @ 6?"0@NNN?N ` 0 6?"0@NNN?N i `. 1 H< ?"6@ NNN?NS  xy =X0 2       2 H@ ?"6@ NNN?N  >c2 0 2   3 <?"0@NNN?N`$  ?1"0( 2   4 <0?"0@NNN?N`* Aa-1"0( 2   5 @ 6?"0@NNN?N @` 6 6?"0@NNN?N@ `. 7 HÝ ?"6@ NNN?N  xu =X0 2      ' 8 Hɝ ?"6@ NNN?N ,$ 0 =- 0 2   9 @ 6?"0@NNN?N ^ ,$@ 0 : 6?"0@NNN?N^ @,$@ 0d ; HĔ ?"6@ NNN?NW 3 ,$ 0 zt1 =X0 2       < 0̝C"?   du := a-1; v := 3;6 0 200 22& = 04؝C"?   Assert(t1=t2); Assert(t1=1);n0 2     > @ 6?"0@NNN?NM  B H ?"6@ NNN?NL Bc1$ 2  C H ?"6@ NNN?N%UE  Bc2$ 2   X H ?"6@ NNN?NX ,$ 0 #i|FCED(t1)| = |FCED(y)| + |FCED(u)| FCED(t1) shares nodes with FCED(y) and FCED(u) No need for normal formFj 2 ! @PH  0޽h ?            <                  <  , - /  , . 0  2 3 5 2 4 6 8 , 9 8 2 :  = >  33s & TIMING |38.2= ___PPT10 ."(+adCDI ' = @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<*9 %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*; %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*8 %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*X %(++0+8  ++0+;  ++0+X  + f-K0  0(   x  c $$@   x  c $%0  H  0޽h ? ̙33___PPT10i.،wD}+D=' = @B + `]-K0  x $(  x r x S  -@   r x S -  H x 0޽h ? ̙33___PPT10i.@+D=' = @B + -K0 0| $(  | r | S 82@   r | S  3`0  H | 0޽h ? ̙33___PPT10i.PBP+D=' = @B +q1 F-K0 ))0C &(   r  S \L@    8  P  C P     H8N ?"6@ NNN?N0P >c1 0 2     <?"0@NNN?N   ?2"0( 2     <`?"0@NNN?Nv  ?a"0( 2    B 6?"0@NNN?NPX   6?"0@NNN?NXP    Hc ?"6@ NNN?N<0P >c2 0 2     <f?"0@NNN?N  ?1"0( 2     <j?"0@NNN?N  Aa-1"0( 2    B 6?"0@NNN?NP   6?"0@NNN?NP   Hn ?"6@ NNN?NPp =+ 0 2    B 6?"0@NNN?NXp30   6?"0@NNN?N3p0l Pp/`  B P/p ,$@ 0 !  Nr ?"6@ NNN?N P p Bchoose 0 2   "  Bw?"0@NNN?NN n Cguard"0( 2   #  Bz?"0@NNN?N E@e Cguard"0( 2   $ B <?"0@NNN?N0 p[ N %  <?"0@NNN?N[ p E &  N$~ ?"6@ NNN?NPp Bchoose 0 2   '  B?"0@NNN?Np0P Cguard"0( 2   (  B?"0@NNN?N0P Cguard"0( 2   ) B <?"0@NNN?N-p0 *  <?"0@NNN?Npc0 +  N\ ?"6@ NNN?N p @plus 0 2   , B <?"0@NNN?N[ P -  <?"0@NNN?NP .  B̍?"0@NNN?NP@` :  CR(c1)"0 2   /  B?"0@NNN?N` @6 `  ?2"0( 2   0 B <?"0@NNN?NXn0 @ 1  <?"0@NNN?N0 n @ 2  Bܓ?"0@NNN?NP @Y :  bR(:c1)@0( 2       3  B䘯?"0@NNN?NP 4&T  ?a"0( 2   4 B <?"0@NNN?N e @ 5  <?"0@NNN?N e 4 6  B읯?"0@NNN?N+%  ER(c2)$0( 2   7  BX?"0@NNN?N.N  ?1"0( 2   8 B <?"0@NNN?NP-+ 9  <?"0@NNN?N-PK. :  B?"0@NNN?N    bR(:c2)@0( 2       ;  B0?"0@NNN?N/'  Aa-1"0( 2   < B <?"0@NNN?NPc  =  <?"0@NNN?NcPdB @ <D?"0@NNN?N ,$D 03 A <D ?"6@ NNN?N0 ,$ 0 U Formalization 2  H  0޽h ?O                      ! " $ ! # % & ' ) & ( * + ! , + & - " . 0 " / 1 # 2 4 # 3 5 ' 6 8 ' 7 9 ( : < ( ; =  ̙33!& TIMING |24.1___PPT10.^/D+JfDg' = @B D"' = @BA?%,( < +O%,( < +DY' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*B %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*A %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@ %(+8+0+A  +) F-K0 ((00 %(   x  c $@    F  P    P     HP ?"6@ NNN?N0P >c1 0 2     <<?"0@NNN?N   ?2"0( 2     <?"0@NNN?Nv  ?a"0( 2    B 6?"0@NNN?NPX   6?"0@NNN?NXP    H  ?"6@ NNN?N<0P >c2 0 2     <ܹ?"0@NNN?N  ?1"0( 2     <`?"0@NNN?N  Aa-1"0( 2    B 6?"0@NNN?NP   6?"0@NNN?NP   Ht ?"6@ NNN?NPp =+ 0 2    B 6?"0@NNN?NXp30   6?"0@NNN?N3p0^F Pp/`    P/p    H ?"6@ NNN?N P p Bchoose 0 2     <dE?"0@NNN?NN n Gguard&0( 2     <U?"0@NNN?N E@e Gguard&0( 2    B 6?"0@NNN?N0 p[ N   6?"0@NNN?N[ p E   H^ ?"6@ NNN?NPp Bchoose 0 2     <h?"0@NNN?Np0P Cguard"0( 2     <s?"0@NNN?N0P Cguard"0( 2    B 6?"0@NNN?N-p0   6?"0@NNN?Npc0   H ?"6@ NNN?N p @plus 0 2    B 6?"0@NNN?N[ P   6?"0@NNN?NP   <?"0@NNN?NP@` :  GR(c1)&0 2     <|A?"0@NNN?N` @6 `  C2&0( 2   ! B 6?"0@NNN?NXn0 @ "  6?"0@NNN?N0 n @ #  <D?"0@NNN?NP @Y :  nR(:c1)L0( 2       $  < ?"0@NNN?NP 4&T  Ca&0( 2   % B 6?"0@NNN?N e @ &  6?"0@NNN?N e 4 '  <?"0@NNN?N+%  ER(c2)$0( 2   (  <?"0@NNN?N.N  ?1"0( 2   ) B 6?"0@NNN?NP-+ *  6?"0@NNN?N-PK. +  <v?"0@NNN?N    bR(:c2)@0( 2       ,  <[?"0@NNN?N/'  Aa-1"0( 2   - B 6?"0@NNN?NPc  .  6?"0@NNN?NcPdB / <D?"0@NNN?N  0 < ?"6@ NNN?N0  U Formalization 2  H  0޽h ?O                                      !  "  # %  $ &  ' )  ( *  + -  , .  ̙33& TIMING |24.1___PPT10i.^/D+D=' = @B +  -K0 @ P(   r  S @     S (0<$@ 0  H  0޽h ? ̙33___PPT10.2+ED' = @B DQ' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* &N%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* On%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* o%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+ -K0 ` 0(   x  c $Pǯ@   x  c $$ȯ0  H  0޽h ? ̙33___PPT10i.2+D=' = @B +Z -K0 - L(   x  c $Я@    - < ?"6@ NNN?NA,$D 0 LInputs: guard g, FCED f Output: FCED f s.t. f f 8 guard nodes Guard(g,f  ) in f , BV(g) < BV(f  ) ||g,f|| = Guard(g,f), if BV(g) < BV(f) ||g, Plus(f1,f2) = Plus(||g,f1||, ||g, f2||) ||g, Choose(f1,f2) = Choose(||g,f1||, ||g, f2||) ||g1, Guard(g2,f )|| = Guard(|| INTERSECT(g1,g2),f ||) & - 2; 2 29 212     5      (     H  0޽h ? ̙33&  ___PPT10 .^/D+Ӭ!D ' = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*- i%(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<*- %'%(+u P-K0 DDl  t r ,$@ 0 ?l  <n?"0@NNN?N P p Cguard"0( 2   @l  <tr?"0@NNN?N@ 0* * ER(c1)$0( 2   Al B 6?"0@NNN?N5 pP 0 Bl  6?"0@NNN?NP p' Cl  <xv?"0@NNN?Nj .@N ?2"0( 2  z g  Pl  r p ,$@ 0& Ql  <z?"0@NNN?Ng  zR(c1c1)V 0( 2         Rl  <?"0@NNN?N   Cguard"0( 2   Sl B 6?"0@NNN?NU p Tl  6?"0@NNN?Np % Ul  <0?"0@NNN?N` ?2"0( 2  z ` 0c  Vl  r 7 u ,$@ 0O Wl  <؈?"0@NNN?NT UN   R(:c1c1)~ 0 2               Xl  <?"0@NNN?N` 0  Cguard"0( 2   Yl  <?"0@NNN?NC c  ?3"0( 2   Zl B 6?"0@NNN?N C  [l  6?"0@NNN?N eC , ]l H ?"6@ NNN?N6pV,$ 0 Bchoose 0 2  B al @ BD?"0@NNN?N; ,$@ 0B bl BD?"0@NNN?N;p ,$D 0H l 0޽h ?`(l )l *l (l 'l +l l l l l l l l (l "l l l l )l ,l -l )l .l  'l /l 1l  'l 0l 2l  l  l l l  l l l l l !l l l l  l l l l l l 5l ?l 6l 5l 9l 7l ?l @l Al ?l Bl 9l :l +B#style.visibility<* l %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*l %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*l %(DQ ' =%(D ' =%(D+' =4@BBBB%()?)?D' =.G7 BBBBBYM 1.94444E-6 -1.38728E-6 L 0.06163 0.09619 *3>*B ppt_xB ppt_y=@0BBAApBB<BD=<*l D' =4@BBBB%()?)?DX' =. 7 BBBBBYM 5.55556E-6 -8.67052E-7 L 0.17501 0.19977 *3>*B ppt_xB ppt_y=0BBAA<* l D' =4@BBBB%()?)?DZ' =."7 BBBBB[M 5.55556E-6 -8.67052E-7 L -0.09166 0.19977 *3>*B ppt_xB ppt_y=0BBAA<*l D!' =4@BBBB%()?)?Du' =.=7 BBBBBOM -0.00486 0.00116 L -0.09166 0.19977 *3>*B ppt_xB ppt_y=@0BBAApBB1B$=<*l D+' =4@BBBB%()?)?D' =.G7 BBBBBYM 3.33333E-6 -3.52601E-6 L 0.05416 0.09388 *3>*B ppt_xB ppt_y=@0BBAApBB<Bf@@=<*&l D0 ' =%(D ' =%(D' =4@BBBB%()?)?Dq' =.97 BBBBBKM -0.09166 0.19977 L -0.1868 0.2985 *3>*B ppt_xB ppt_y=@0BBAApBB.BBڸI=<*l D' =4@BBBB%()?)?Dq' =.97 BBBBBKM -0.09166 0.19977 L 0.00486 0.2985 *3>*B ppt_xB ppt_y=@0BBAApBB[E=BڸI=<*l D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*8l %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4l %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*>l %(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*&l %(D' =4@BBBB%()?)?D\' =.$7 BBBBB]M -8.33333E-7 1.90751E-6 L -0.06667 -0.08878 *3>*B ppt_xB ppt_y=0BBAA<*4l D#' =%(D' =%(D' =4@BBBB%())))?D' =1:Bhidden*o3>+B#style.visibility<*>l %(D' =4@BBBB%())))?D' =1:Bhidden*o3>+B#style.visibility<*8l %(D' =4@BBBB%())))?D' =1:Bvisible*o3>+B#style.visibility<*Pl %(D' =4@BBBB%())))?D' =1:Bvisible*o3>+B#style.visibility<*Vl %(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*l %(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*l %(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*4l %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*]l %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*al %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*bl %(+8+0+]l  + $-K0  P(   r  S h@     S dpP`<$@ 0  H  0޽h ? ̙33& TIMING |92.7___PPT10j.[ +M{D>' = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* :Q%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* Q`%(D' =4@BBBB%(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<* %(D4' =%(D' =%(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<* 1%(+? ?-K0 >6X (  X x X c $@   x X c $|0  B X 6D?"0@NNN?N `H X 0޽h ? ̙33___PPT10i.+D=' = @B + f-K0  0(   x  c $@   x  c $0  H  0޽h ? ̙33___PPT10i.،wD}+D=' = @B + -K0 P 0(   x  c $H@   x  c $  H  0޽h ? ̙33___PPT10i.@+D=' = @B + -K0  0(   x  c $@   x  c $h`0  H  0޽h ? ̙33___PPT10i.PBP+D=' = @B + -K0 pD $(  D r D S l@   r D S ,0  H D 0޽h ? ̙33___PPT10i.t+D=' = @B +V  -K0 H P(  H r H S  @    H S 0<$D 0  H H 0޽h ? ̙33&  ___PPT10 .Pj+YD ' = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H t%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H %(+} -K0 |t`@  (  @ r @ S @@   r @ S 0  B @ 6D?"0@NNN?N}` B @ jA ?txp_fig"6@ NNN?N` jb SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $$\frac{s \times k}{t}$$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH348(BOXHEIGHT200"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG FalseD*ALLOWFONTSUBSTITUTION False6BITMAPFORMATpngmono&ORIGWIDTH486PICTUREFILESIZE3365H @ 0޽h ? ̙33___PPT10i.+D=' = @B + -K0 @ 0(   x  c $@   x  c $T0  H  0޽h ? ̙33___PPT10i.v+D=' = @B + 0 0 +(   d  c $     s *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;Ύophr0 UN^|ev0Dia)] l#0m038ՁsPmg j#yEd=w| Pm Oh+'0T hp  PowerPoint PresentationoweoweSumit Gulwanise1229 GuMicrosoft PowerPointon@r2@@GSg  )'    """)))UUUMMMBBB999|PP3f333f3333f3ffffff3f̙3ff333f333333333f33333333f33f3ff3f3f3f3333f33̙33333f333333f3333f3ffffff3f33ff3f3f3f3fff3ffffffffff3ffff̙fff3fffff3fff333f3f3ff3ff33f̙̙3̙ff̙̙̙3f̙3f333f3333f3ffffff3f̙3f3f3f333f3333f3ffffff3f̙3f3ffffffffff!___wwwff4'A x(xKʦ """)))UUUMMMBBB999|PP3f3333f333ff3fffff3f3f̙f3333f3333333333f3333333f3f33ff3f3f3f3333f3333333f3̙33333f333ff3ffffff3f33f3ff3f3f3ffff3fffffffff3fffffff3f̙ffff3ff333f3ff33fff33f3ff̙3f3f3333f333ff3fffff̙̙3̙f̙̙̙3f̙3f3f3333f333ff3fffff3f3f̙3ffffffffff!___wwwnnnm⍻nmnݓn⽑lmsüޒⓑJlCmCCJngnnnmn½mnnr⽻m’mnlnnnݓmssⓒmmmmnmsnnn⍻ls⒵nsmDnnmmümmnssn⒒n՜.+,0d    On-screen Shown-se{ Times New RomanComic Sans MSArialcmsy10Default DesignMicrosoft Word PictureKPath-Sensitive Analysis for Linear Arithmetic and Uninterpreted FunctionsSlide 1Slide 2Slide 3OutlineSlide 5Slide 6OutlineProblem DefinitionFCEDExampleExampleFCED ConstructionFCED ConstructionNormalize Guard Operator"Example: Normalize Guard Operator)Randomized Equivalence Testing for FCEDs*Randomized Equivalence Testing for FCEDs OutlineProblem DefinitionFCEDFCED Construction(Randomized Equivalence Testing of FCEDs*Randomized Equivalence Testing for FCEDs Conclusion and Future Work  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles%_ Sumit GulwaniSumit Gulwani  !"#%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)Pictures!GCurrent UserSummaryInformation(TPowerPoint Document($DocumentSummaryInformation8