ࡱ> lo|}~mnV(@ / 0DArialiKakupopta``/@ T0DArial Unicode MS`/@ T0" DCalibriicode MS`/@ T0"0DSymbolicode MS`/@ T0@DWingdingsode MS`/@ T0PDHGPSoeiKakupoptai`/@ T02 B . @n?" dd@  @@`` (  -' "%./01256       ] - D1H         &1H1 *" 2          )   0 3ff3@ʚ;ʚ;<4dddd,#0,g4{d{d0<@ T0ppp@  <42d2d,O$0`)___PPT12 %0___PPT10 ``"___PPT9{'w2{_(?  O  ?r E DsSpec#: Research Challenge   How to verify object oriented programs and in particular object invariants in the presence of Callbacks Aliasing Inheritance Multi-threadingFa/C3f/   Demo (Spec#)    GI'Lectures    Verification Condition Generation Logic of Object-oriented Programs Invariants and Ownership Abstraction Multithreaded Programs 0 "    qt Boogie PL  MLimits of Boogie PL   Boogie PL does not contain structured control flow structured types a heap expressions with side effects visibility subtyping dynamic dispatch0 t 3ft&t    uvBoogie PL: Code   BCode is unstructured Code ::= VarDecl* Block+ Block ::= Label: Cmd goto Label+; | return; Cmd ::= Passive | Assign | Call Passive ::= assert E | assume E | Cmd ; Cmd Assign ::= id := E | havoc id Call ::= call id := P(E) Variables are (weakly) typed VarDecl ::= var id : Type Type ::= int | bool | Array |& Array ::= [Type+] Type Remark: Types disappear during VCG; they are (if ncessary) encoded as axioms.6   Q N 0 -%  AN*!        @    Y        U   `DBoogie PL: Meaning of Code3  . For any command S and predicate Q, which describes the result of executing S, we define another predicate, its weakest precondition, denoted by wp(S,Q), that represents the set of all states such that execution of S begun in any of those states does not go wrong, and if it terminates, terminates in Q 9 p3 3=8&   SwVCG 1: Passive Commands   "assert E - Programmer claims that the condition E holds - Verifier checks E wp( assert E, Q) = E Q assume E - Programmer cares only about executions where E holds - Verifier uses E as an assumption henceforth wp( assume E, Q) = E Q S; T wp(S; T, E) = wp(S, wp(T, E)) C% f%C f           L            xVCG 1: Examples  jwp( assert x>1, Q) = x>1 Q wp( assert true, Q) = Q wp( assume y=x+1, y=5) = (y=x+1 y=5) wp( assume false, Q) = true wp( assert P; assume P, Q) = P (P Q)        )    , yVCG 1: Assume-Assert Reasoning   wp( assume P; S; assert Q, true) wp( assume P, wp (S, wp( assert Q, true)) wp( assume P, wp (S, Q)) P wp(S,Q) b%,=*==                    {.VCG 1: Correctness for Procedures (simplified)//$ / Let proc M(par) returns (res) requires P, ensures Q and impl M(par) returns (res) { start: S; return; } Then valid (M) = wp (assume P; S; assert Q, true) = P wp(S,Q) We will refine this later. D=  6    :  0    eJXv_ VCG 4: Loops    FLoops introduce back edges in control flow graph. But technique can only deal with acyclic graphs. How do we get rid of back edges? We showed the result of this transformation earlier in the slide entitled: Spec#  sWhile Loops to Boogie PL In detail: Duplicate loop invariant P by using assert P = assert P; assume P Check loop invariant at loop entry and exit Delete back edges after  havoc -ing loop targets &Zl!Z Z" ZZf"K'^@     &'()*Tp-_.$uSummary  Boogie PL is a simple intermediate language. Boogie supports Modular verification using contracts Linear (in size of the code) VC generation A standard background as well as a program specific one 4>  |Appendix: VCG Example   start : assume x > 100; goto loop; loop : assert x >= 0; goto body, end; body : assume x > 0; x := x - 1; goto loop; end : assume !(x > 0); assert x == 0; return; & Z   &  @  @ } Create assume   start : assume x > 100; goto loop; loop : assert x >= 0; assume x>=0; goto body, end; body : assume x > 0; x := x - 1; goto loop; end : assume !(x > 0); assert x == 0; return;  & Z   <  @  @ ~<Move loop invariant into Loop-Pre-Header and after Loop Body= =$3 = start : assume x > 100; assert x >= 0; goto loop; loop : assume x>=0; goto body, end; body : assume x > 0; x := x - 1; assert x >= 0; goto loop; end : assume !(x > 0); assert x == 0; return; 6    Z0  +  J  A SCut back jumps: assume havoc on variables assigned inside the loop;block loop body *T R$3$&>     start : assume x > 100; assert x >= 0; goto loop; loop : havoc x; assume x>=0; goto body, end; body : assume x > 0; x := x - 1; assert x >= 0; return; end : assume !(x > 0); assert x == 0; return; 6     "@1  4   %Create Dynamic Single Assignment Form& %$ & start : assume x > 100; assert x >= 0; goto loop; loop : skip assume x1>=0; goto body, end; body : assume x1 > 0; x2 := x1 - 1; assert x2 >= 0; return; end : assume !(x1 > 0); assert x1 == 0; return;         @1  1   Passify Assigments $4     start : assume x > 100; assert x >= 0; goto loop; loop : skip assume x1>=0; goto body, end; body : assume x1 > 0; assume x2 == x1 - 1; assert x2 >= 0; return; end : assume !(x1 > 0); assert x1 == 0; return;       @1  1   Apply Block Translation and wp0 $$&   start x > 100 x >= 0 loop loop x1 >= 0 body end body x1 > 0 x2 = x1 - 1 x2 >= 0 true end !(x1 > 0) x1 = 0 true start         h 0` 33` Sf3f` 33g` f` www3PP` ZXdbmo` \ғ3y`Ӣ` 3f3ff` 3f3FKf` hk]wwwfܹ` ff>>\`Y{ff` R>&- {p_/̴>?" dd(3fx?" dd  " @ ` n?" dd@   @@``@n?" dd@  @@``PR    @ ` `p>>aN0 og  (     Tn@ ?Rectangle 3073" `} @  X Click to edit Master title style!! F  N q@ ?Rectangle 3074" ` @  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S   N}@ ?Rectangle 3075"^ ` @  X F     N@ ?Rectangle 3076"^  @  n* C   Q   NL@ ?Rectangle 1029#"A5PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!$K drs/shapexml.xmlVn6}/Zx-ɗ* ;m70eH'EgHIE~G&9sf̡>92 c+2|Y$TJ33bu\\j%24r/m"Uvdl\3vm5t#Jmjh+qjMxuk^)v gjln0QULk9@8n32ֶ* DajPjbj~^X\Bl"ݮF՞3' C>ܼdm}zSwN*|r(M}~NIeҳ v08(dž4!ǎ0tB;cW?WD2fZ-ϭJVR_T;36rQARrn@Y,rQʝY>8{&sZVE~]$ꌍbt7hy0bע`Ax%d'J+wY堎1p.( uЈsFlyFJniP P~u?H`^^pUƨgneXtOЙqS ^&4فjf^`Jse-!"-v*Ggm(Eu3fuZw()Ӝ]IA8$Vy_J(. %'Z^ia'H GKhGq N6w3n:m^\$_i{IV5IraЕjWIȘPopB^EH3Rz-mtG'YidE5~ma.&TA(O}7>Q GE5UۈPk;E"&I8Si*pПt=/ jfr|{/PK!Bn" drs/downrev.xmlD]K0CdZ!ls]޾6&I xy8<3_Z4unD NND΃PhC9$t:(0K}Pr Ԩw6VTX[Ut،TAÄ_%c8Ig4>xv}]6yxsoaZU ˆ_&AeKh9a.~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!$K drs/shapexml.xmlPK-!Bn" drs/downrev.xmlPK*^ ` @  r*  G   H  0޽h ? 3380___PPT10..f#PK!(b[Content_Types].xmln0 EAkP }l} m $_tI$svs^챐KkH$Q -G$oo1# ɩ5 J# \Qg0?0omRo?Y8 Jm i|TX+N3tr@9>?4 ΠMfrAsѺo_p?yjŝ & Xg3PK!*8 _rels/.rels 0DnzЃXmlo0of5OIw AN{cݠv=m 838yG 6U} ShLq`L)d=Ҍ\@.;3, ;$e͂): vq}j:zɥ'k茜(f,ƁXA6\m>PK!`.Xޏ$!drs/slideMasters/slideMaster1.xmlMr0 cV1oz`iYq+9Qkl  %Tpo\H EhB7 !IH` ݋4=>Ox7BZ{IR+"˷J@kWX]Mi"I~뮞^wa/ sBug\djV{a7UZp>!_5|e~sM ҠSo}WՂCN| <p{/L]V`=n; ʝJҤj>Wn+ orAr]hM1ѝbg-_:G, ޲xHT1@el+b-R2td۩w 2YjŹ1l`MM; [#kQ\H %}񲵗U.dEG_h PK-!(b[Content_Types].xmlPK-!*8 *_rels/.relsPK-!`.Xޏ$!drs/slideMasters/slideMaster1.xmlPK.PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!ŖL=7theme/theme/theme1.xml[[6~L{c ÙdiL;9YcCﻺadlɡIڞIdyZIZq^|(iUї/ ]Kˤ~ZrL7zY%kj=kb$Ѝ1-]Up b[OP,LpRJ|QV&ߗ .`mHGRD}z7ڒj~Idzݠ/}qr@}q9.}oE;s Q$0Ae{B9m$~k`47 j /YO5|Q${wfdF/Siť;]UzQ | VQ:9wU@|(pZޚu bKqu%Y/;嬺O`TL$3E~):ɦ*-N;C1&In_cڿ6{arpF;V |Q7eȵlpڲnN 1ELZ?o%S[RӨHS {8tv aDTb$HdYBY6eC&/Ñ93G\VGIἯn.%v:9΢>mtZ|uޔ{]im?iŇ ͷ!Ӏ5ey8fC,"<n I?\4eGC6oڍ]c0%Y&[b=2d}Hkmn 1TCڢk`\ g rQ|_knLZ}:i:MetcZ[F cz7GkK}!pHhY6~LZ/[x"xܷdxܓܥ$)8t$4=B!qBF3&d4"lly ]`4"(rft'T/qtyxN=BMQ@qi`NSbzĸQ_4!Ɗcdel v`AhQft9L8jNքo}r}i?)=;~t3II5ȤXfYO'cKȬDJآRN^=ъH16F-΂C {` XacRdC|ƗF~ʊO(!yw(eo_$CQ"Yv};k݆U2gZ@%\>4XL4I bzC77K`2)"6K =D9@ <_ x=6[CqYw`dճaw d6 %l(t:a5lGR!&lrvO5W2|YsI.nQ~6lGlجXFZ };Gb<66ͤ6fDf* dC-K `o;66o|gywϟਐ)z6OW)6NP6p |졔tm|?p%lY+I\z6aC$@$@$'P4`kwWac*Z.M"H^/ E ^{oI~/MlT&L֯:-48l"7ʦ%i[ظWacUf ;Qڻ9bYҥd#l|#eTV!kӭ8lƒLjlg*lKܜ#?H8y93mb+z%[S ;'qU GOmל JXh#l g%{ |q\'#- 2=B7t^ۄ, N~ gE&t-" nPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!};7!drs/slideLayouts/slideLayout1.xmlݎ +OUUVv{@1b@@\{vM# 101aq֊4yiN'M)nI7W_()ŒjCoV?,lUyf$ْV!<,M59Xn]Z(HCq(nVyx&WDgCTpL붝vfbVUpOhA,z"=6!ރiگ,&j F|vj,&F; U4NW%D5'O06eL1 YTnSjb|YqSI7^p5%fB5O#>LؽDOV5}lRxd,c)-_PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!};7!drs/slideLayouts/slideLayout1.xmlPKUPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!M/"N!drs/slideLayouts/slideLayout1.xmlXr6}L׎#Swk,gbn38- ,{v td/,g/]464>qJ4~{6^ k9 u~bbj& DLõsŤӱZf~ &桳2 Йtχ^'=9!O4&ڕ0F*᠀]Њc #-`xs4߅ -& 01Oc12xJ:݄elqo$ibnxvntEP"/Ưbt?THbKLvu)&I3=ILq9׳+W;P(5Qnb- D{JQ<~Ρ'_m+0ҙuPߥNI/W.=*y6.D4vǠ.4 af0zc>B!%t1q|L&]3N-tA%me=+㭊p@!d%o/{yk l*Aq)EyQi<_ul6..Ca1]+J[{mv`@崓܊ gEӜ;Ѡ4EoQD &\Bđ0x2,la>k; /~sx1͕ekG8p. fzQ^+d̘f^!Iѐx!3Q^Kd1 K(/.| ^xq,[xQoQwA= xAp,p xa tCBϞ;AeB8 ^4щN!fbVÖ 79q} @{\ uE y3}my}⤻]kdPt (Is[[֐ɡ,e%>%Hm܆_]nnqD/7_Arf]# Γz5FPydimT@%PP{a2LF 4b)%z)J_ߩEůduRks Y:M36W&X>JQ%&Bkk$qfZ I&]eL{cn(?fzp-gQbA%(b{[ju\lb#[loS:k_ws/1JM)Tu>U+jS5e*{l9Z 鸦-L IFrCɡPVyN,]@FTZh-χ4/PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!M/"N!drs/slideLayouts/slideLayout1.xmlPKvPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!%,% N !drs/slideLayouts/slideLayout1.xmlWݎ8_i} ! 0@LU>I$[ǎ}=c&2J{s|;';RELx\>TKi;zOB4)]u:5Y*ڼ5x(W+>Q4h)A am2{ЎF1N5hn<[=V]7Jj8,7<bj0Xls"hG bA1fbe(R憪Ff 0?z&Z1!Ehdn2{͊gY z7My;κ5#+Xz' ~{Γ }]~]jZ{i񍍩78l8&hb(b"IzTDt_$NiFڍ 9oZ82NS!l#?8ꁦ9~T"u0ocp#wxl"$x`)-xm/DKROL5-1҂c"+ ]>Uչl9{aV5?C68!'MIc/^ Whyg.DTs /BPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!%,% N !drs/slideLayouts/slideLayout1.xmlPKpzPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!"G~!drs/slideLayouts/slideLayout1.xmlRj0BFI ؁>/mH[YMbw r1ٙюEk k4ڻ&SδS&_7θ|__̓x&F.JxRBDUi qv+=ZHtč(q;ދ;av|pK|YJ?{ڥ jĪqt ԑlzPi(YOĆ)Z9< *׼aXf.:bh F8oF'm6G`miYK"MLAuDU:RL=4?NPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!"G~!drs/slideLayouts/slideLayout1.xmlPK`PK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK! !drs/slideLayouts/slideLayout1.xmlSN0}٥RUE u })L7C}Dyŗ3g|`4eيo/7I+\OۋEۂvVV:~]eQXB;D_E4/r' mùh%j{0,g餄ċ' 5 qaaAF'P˃#gz nyMF̂1XL eZw  L`.Ŝayk F]yar8S$7Pq1T)(^;|bi@'X&U\-rdU*s92Hg?B4'z߱7ϸ)XG ~ƽymg/V>ՙq#+)Ko~;:_5*=d:s)mkEvESv$U޵hчR\( E`5G_$\XĤ[Շ+.R K8ٲ-#)x:R,p>0ݲ幣`<-nB B"i'٪ao`hţ\X2 k%%hX[m,kۉڊZ`mub-v:XS@(6gC=#Uv0FɔDI&RW),$wʍSЌ EGD\!Y>1laHRw&IvM;O&~uDop-iQW2yDHiïKn*/fceFsY/ԙed?*'L͒3 "1$6Ǚ8ډhl'OHܐk Sإ@eo Ʃ A,˯ڤnZձ#JAS>Ur;~2'i[-vN$ZbS)uz%Sn »ph'2xnS6ͰtP_`u`;:[b=سC{~usDƸ 3clvDpV1~;VgYtI_R>+Ĩ>h{?Vwͺguʳ1ugz[wlƒYx*Qxܽi/R5-o+w9uwyzPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!MQ~ !drs/slideLayouts/slideLayout1.xmlPKZ0PK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!;bE !drs/slideLayouts/slideLayout1.xmlVn0?'z![i$%:BQɸvd;i 89]{v$[ mZM4 Py]a]f,W@&32@(IKQqsZ7BamQ[|ꇰ7+&Q4 {aKz(sΟ*Br̲lLhav$e7 6"!x0gW)g`W32ڭN Avj]7VM׫[ʂ@A.fS g녮g<l= bڲO|ymu9SN҅3[Fx7zU珆qR>zՁQ,ޖV/:=:{4nH~4G/DI4c4qoD9C7] I:?2|Yd-m4vf7)x%cc\>PI )g;] bp)[Nd9"t@$); YLe?B3' /hu@υL?P-vt{WIû򜌣a?+yDQ<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!,S1 drs/shapexml.xmlVo0~M!*TЕu8ؑ0}wvR*I<$Nﻻ.\rL1omq&TLmirfVb̕7ϟ *cuMoE.B[MͦYarO.Vk6saj*V~iXy39|12H:YaB;[Q᝱`J M.GMI!#r[l;H(qN]8CjM!igwtv,1oYLw,F[oo# ,Y~Fs BuY1䡈a#!x\R1-2j™qV׌HV 1{r2lMD Ռ][)*j/@M}X̂/Щg*~˚6CO^!Q#Ҙ6P3#ET+7B4gVUfܲVY*>RBEnѯ[L5ـadʺ.oy:>Xx}x!A V(={Aӹ5:a7޴fy>8'\y)Q0X]g`\ u(4`k+l' h/pPU";Zq VȌ6VL:5)]gReKtSa.bߢDb -JxITk/b$%W g3Cl+!aZ߇) (~W~:Td h}ۅߙ/)PdqPK!drs/downrev.xmlD]K0Cx\b [W EЮ M1eݿ9ͨ$ngЕn(&ӜIm`XA/B&)І`S} X6N0E`0!sc:=]̊m+(| x\j/|qNKC{sYdSOO xPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!,S1 drs/shapexml.xmlPK-!Ndrs/downrev.xmlPK_ ?% 7  p* C    @ V1? Rectangle 82947"@XK   @ H̤?Rectangle 4"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!E\ndrs/shapexml.xmlXMo0 tZۉ1NhwicˉY$9KGIN6 R+٤'>dÔ.HitRD&R,Szw{y4D9p)XJϟND )]S'A@˚ RU`V-Z1̈́q*p JA'뙲z3SS:D@1oXwD1ZP_ ~bzP!ñ$ [h! (E۔۹~.vA-Tu8 $(pTR0 ,H֐ a8 paz,ֵV\1]* 7 L|>qz6lϑJi)}u6b-#T(/$Oi,dzȢl!6:fnvX`wq@n_ &`7n7.#R_x9%9+na1qӐ`*7)0gn pTh8eZC}㎋yYLf!e~\#DK^v\yַ/ܧ^(P{Zhik2odK%i{ 20L2d-6rowmpo{V^qoliK:u*J{"wRy^;wx0λ1Q kK;t/C1zDxdN2d>do??pPד_PK!_jjdrs/downrev.xmlDKK0!\8΃N b:e$N7pn=9V nfTY|+{Ұ۞mx$<&ޡl4 lPr;*UH|45-{z+:_4|K2V1CꪗǮ[`bprcZ/·bDvWbx@/xg`   PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!E\ndrs/shapexml.xmlPK-!_jjydrs/downrev.xmlPK )  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S  @ V7 ? Rectangle 82949z   X C    @ N诌?Rectangle 6"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!JGeJ drs/shapexml.xmlVMo0 tMtv~cˍY$9K;Iۡa@v\,R#H xvęP.*u/w׃9g֑*Hj%24yچᬲisM:|'jou#d659|acʑZFpf]w:lci^S˒x1ǨCtPP*^a4OrhL( #o1}bT JRJuY$7fIq:`3y8yeAkR92S*۸pdA&/#y62!B$IwХvRF]e<j:! dV!~,nNûR:2,{ hE2x`PRK J܇)Ns&֪͊[*$$CM{L׹cd}.~Xu6j8,P?um{)1T}n-8FR+رJKYc9_ftp5 &d9Uru$Q!ބAUm]k |e\M).XlUbg=Fқl/܁a9auMN*?e(>-Y!+?Q(Fү=0SJtܱZV02q`B(KL>JuynnXTR@oj5.vAQvAZ=>߅99kX!? 6 d=⟄m.~PK!1drs/downrev.xmlDQK0Co.ˆL2|Ve-6IMpzRкh3uedk>I8/AX./"f;_.RW5u*C5V:161UAш7 V q[?|(DQ'ί; '?@0l62>Q$;%a[Yr`@W?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!JGeJ drs/shapexml.xmlPK-!1gdrs/downrev.xmlPKx ?  p* C   < @ 0.k ?"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7drs/shapexml.xmlAn1 EHC=$S$Fa #'J7Ă;_zϿމ+<Ь1r "d.0icvlSNV=PK!Bdrs/downrev.xmlLAK@B2ovb4R<(m{fM4;viwK|0Ǜh;1hZng͵S- #uv,'WxM4"epIBc#іNoPy:l]-^4F׿<h +{3R^ODcLmvn*NBZgNIJ?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7drs/shapexml.xmlPK-!Bdrs/downrev.xmlPK I}OPM80___PPT10.q PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!,߼etheme/theme/theme1.xmlYKo7 Hȁ%Kq81,%E.˘\ߊX@Ѵ@o=m$@/qM]ֵ!~fr~4.DG4I3nֻ\*!)A0=$J囵 aK<'|rb"Emjkz֬fp S4֤VI?`)B&Fx3 6:lh<}&f$ExLu7 S@ X=:\3")90 Acg8 +l e~]oxFkoXR%z^d%|w<Y|g ?ixJu 9dn%|@籣ELy΋b dX Lq1njN&;ʥ!- P\ur {컗Ϟ>xzӇO`8݉/>B?ţϫ?Y5P_<_~۷*O\Dl3 kN&'3X k)x' \+xG@}^%b {]OR9qQ ׵,YW 3wQ><f9FZEO>Ù1ɈB?$bR |]zV.ɘNhZLڥ)JA6{wP*wȑB1a2^3*1N7J ODŽq4Usn qunc'Vq~OpWaG4K\B}{~ٹCm{*-D K^Ni"\L3u<"⻃g>x_ށ޷7xkyj]Yϱ is)elN!M,aÈ0癓 b$dFIbYP\vxhؕ=pSg9vbs,55š R0U5R+KkLM.ՄNA܁ Hn¥[^d#b2 iK+ v`\#Gz;iei8JVR /ij279YA:@!λ"xJspԽf1\Jب0M/ypcqNye R`0Hdd_kC̼&mZRL$Tr|%186\Z+8(KN[1l}\Vx 7uu.Ҽ9ڀ)[VѼ%J])B#L2eem/\ poFz}Cz\C=rDž@p_1Y.,hF%} 3Q&h.$+)L8 ˼u01u\/+{cw}Ɣ46¯9%#cdhn PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!,߼etheme/theme/theme1.xmlPK-! ѐ'j theme/theme/_rels/themeManager.xml.relsPK]e ; h   D (  D D Ph׌? Rectangle 83969z%   T B     D P? Rectangle 83970 ?%  V B     D V\? Rectangle 83971z   T B    c  D V? Rectangle 71684"QKPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!9{:c  drs/shapexml.xmlVn6?e`'t70PeH'E璲' b]M%^9X)v֕F'ÙԙKIׇք3΅2Z&\>3W3nV'|}=k]pL-5 c+h7J'q*u:v]R+8Ӈu+;ܖJ]ކPҗ;b {$Jx,uzÙP)6T l*H*+LC5W7` ؕ9S1h<{Q. 41҃H\BPG'dk3ʷrGB3 RNˇpÃ}:jz]g  BsquP]bvt0>Rd,U#:0W]!I~ZQ寕K'$/myl EUoE|=#9M>y JZ *6PxĜ™%q49' %A镰K*as\Cay r{ @"h-R/.oB6Md*yKw@DAwPF>(b'EHbV<M&ݛho 7֠?&y5-:^5X׸ɅTvep[_PM>7HfVϕ!g[x$>_SКjx>BsDd7},Df<--^J7kS$B?hR jJXAhozv &WPK!8g drs/downrev.xmlDN@E&3qc`F(H&[ PƄ;[tJ#Z`4 .ht {@Zpi42ˋ9_ޡ]޷Qq74-+UVTX~J ;xX7 \?t"Y1v}=>!$;EkIW\3 &qx\lm#R3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!aYKtheme/theme/theme1.xmlYMo5#d4uS%ڴQv[ԣw;3ޤ( 7J\ʯ AxmYlKPթۏ_{/_3tHDK"EZpI3^NTƻ\*#9A0eJ덆5xI 6" EH>9k,7V#ǴPs{s<1AC-4ڨ<J1-T# *9XߤHG]&!fiq+SmsU ,'ǭ5<q 7 \wl|B ^{1s@ve۞=dsromPhq0n6pU)dNnw:3dZ3ZŘʫ [s\l@?0hqI8bFGj{:*s.$cAKՉ>(1Lދ߽xx? 7!͉D79f[NFF 3LE*qQD DcH VALm|"H0pcVflUO-ܔTyrW_6ԕP +Ui$TKYr}Uoze+U`^'Beh-И+.0|qT{9OS$(0*0e\aS1l%] e [Nʞ!aCA)RW" q -1Ju$K-qͣfkvpuk@!ߖ,.Ԥ4[,_sKs w/c$U=]Ehh,MNV~*bf$|S2 oc¬707`~Fr᣻g܃c7d`\Yk5PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!aYKtheme/theme/theme1.xmlPK-! ѐ'P theme/theme/_rels/themeManager.xml.relsPK]K ; 10aN0 0((    3 H7 0e0e ?Shape 2049"hbPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7od%Sdrs/shapexml.xmlU]O0}`u!P"@bT3uؙ¯߱@4i}׾NNbi]mSΤ\s<钔r̵᧓ϟNµ /o$qb)r؆<>itR{xQIGAPflffY]y"M /,KOz΁Ԉ듡I`|3bI^YkJr|U#ՐMdEۛ+`;y6GGltv"n*m>arB*ǏS&i$[0˃ igtD]rm| t9Z٣%~ɂ:] ϑp`,h0jaDZ j%?VB9?OJ~11 XmN#QPTKLOOcRig+0;{IS}nW+YtZ buKht l`AQ ,3نv_zob뵋7Hb=~/peM<-Gl\,Dtp?TN*,]1uG*{s,7NLai弭WqͣJZ{ +6x |:ͨYc(_(I1NHQV82\Fv`+fV%BqHțH/u%qU$K|>VSH½S <ctXQh|cYBtwwcDN~PK!q drs/downrev.xmlDk07؋Ju0؆5_Jm ~-ףn2`6HPX38(xkP2@Ò' Ձg`ps]BH_5R~j:;DX>xnIHiLDs~YPDG8>ݐ6cOccN1n4m%?nB- `?<NV= (PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7od%Sdrs/shapexml.xmlPK-!q Bdrs/downrev.xmlPKW> 7  0Towards a Verifying Compiler: The Spec# Approach1 1 1 @   3 8 0e0e ?Shape 2050"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!? edrs/shapexml.xmlWn6?Yˎ$BE mca`DQjTIqHIh| i73O]VZW3)*ow'9O e̸6߮5 kKoȉ}2qiGNjOj4ItTSY`/ۥeUIr6LScWkj$Ýn!'C?La `i&jnפ嵵i-p6N\5R 4kJre|:^'gn6u7c_Qjʒx?r@l$!@ bd".&S<9~Qǰ(/=Yߖ,Sk}9Nӳ .쏞ǫ[2 f jD_@J+"AE]jhmC1[ YSz .^BMJu\ buƒ瘅ecAQ ,Kٖ8 o#ndy^{ ["Hoޮ^^;@y=!#_&z+ (nں?UG,Pg\o+< B v9oMU8H ^BW *(g-1e]oOHQ]T㌪p3V$~ՋTR y,K)[=m8cDe+I>Q:pH8{E=C~%YBYɎƮc(黨ўn׫~(܇ 0h O o{jE{{bx2okPK! drs/downrev.xmlD]K0Cx\:˨ˆ ] :?.m޵Y&z0<^X -C7i2{o,w2ߜ?JrMd]8%t/PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!? edrs/shapexml.xmlPK-! drs/downrev.xmlPK ,  7  >Wolfram Schulte Microsoft Research Formal Methods 2006 Joint work with Rustan Leino, Mike Barnett, Manuel Fhndrich, Herman Venter, Rob DeLine, Wolfram Schulte (all MSR), and Peter Mller (ETH), Bart Jacobs (KU Leuven) and Bor-Yuh Evan Chung (Berkley)  ) "C "  /Zl     Q   @H  0޽h ? 33___PPT10i..f+D=' F = @B +0aN0 RJ@((  ( ( # H @ 0e0e ?Shape 75777"YSPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!Ԋ7drs/shapexml.xmlUmO0>i׉BiDmR* qhcgS ~B5M2iHws/m*Һ9Z):8y9)eʵgϟN %uʗIRV侚Zj c+8ڇ^mړGJqWQ ܲ2OhN drs/downrev.xmlDQK0C/nnuӱ!*U|͚6IJmpgtye t !S[LZN A):k_^D.t*CDІ爾nI ?="DN#[wxޣĉVj>Gapg]OtTjX>BhװInq?G_qG)Yq`PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!Ԋ7drs/shapexml.xmlPK-!>N 4drs/downrev.xmlPKH `}  8  jThe Verifying Compiler    @  ( # K8 0e0e ?Shape 75778"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!qod drs/shapexml.xmlVQo0~`uJA S[$T=OG lCi>Ih&eҚ컳ᄏӾl'-Jyc32>nN9TNR+rw N딯Ib~ԵPT5Imʑ;LYrTT*>ejKnaX|<')rM`']t!D26߄z@G0?ǫzM^\ւrrBlUGS{JS>L`2j1.8dkC4z} `sz=/#xcei3SBVgĺhtCy0dgԓp\؄\835'L95ٸ#h&s .+fLjpyXlUGI`󂭳E؎pm翦S[\Mי⎃em+ahWkivԉ7H܂ܺ o 1 0Xf[YFpuʅ:03&[Oy YgM e8 oc{ GS,ėg-Em宥pQ**}SJ'V2^hVX"YU /nE!2⶝׭Cv+(C*u"]&t=Rdf ߏ tG6Q׃I΄F@a o /zk YiGHH߈?iˢƃgTO; :PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!qod drs/shapexml.xmlPK-!, drs/downrev.xmlPK 8  l  A verifying compiler uses automated .. reasoning to check the correctness of the program that it compiles. Correctness is specified by types, assertions, .. and other redundant annotations that accompany the program. [Hoare, 2004]N /3fB53f.  @H ( 0޽h ? 33___PPT10i.џ+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK " S0aN0 P,v(  , , #  0e0e ?Shape 74753"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!iGdrs/shapexml.xmlUN1}ZAn h+E("&^kom'|} THqƞgΙK7dkalU{]΄uQ^pfV"JOgMjʦM5icF(JmjrؚNcʑZvqgЩR|zL԰0%)wF04.^!D2Ҷ߄Szw0/H= cBPa1A #Q1&uK]EB4mwC. K 5\j.¥9Y/Oj=0]zCP miؚlR"-.EvWI^7vvKs Wx/kL`h>.`fj vBSRjrUW~"@qfj`/<(ʏ832 Y8[ }m|yHQ'oYytSud[!JW*)#xb xcU\l )!o^e)rm5Q-+歹CiVR_B"mG 1gb]<'5!OD>9w?2?vDی~PK!wx drs/downrev.xmlDQK0Co.nec(!Li+owM֖57Y"siIP[0` j*%|䫛`!")l,i da1alK>edB]y(*m0 w; >+m6 q5:Tb '{N7sʗWX];jft+?d_ZI&ykbK?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!iGdrs/shapexml.xmlPK-!wx <drs/downrev.xmlPKP}  8  'Spec# Approach for a Verifying Compiler( '$ (  @p , # n8 0e0e ?Shape 74754"J D PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!Ib drs/shapexml.xmlXn6?YَBE m0s@KT"Uv[i!e;1vB>$gHμ73Vl-x]3sST1N.8s^B(eƵﯾI]ðW&M/d-;H Yil-<1itR{qOAw&4az=kF/eUhę5-D#- y-LLt9SX,ahNۅЏZ󴐢p`Z cɚfs;x0`<ƣv_T{o]Zu)RS.cΞaYGc/R,b0c`4>; fF[Ѹ&xE;y?hDOƾpd0w5C$™}-xukTƱCf3S7O[Dg%w!M# XvS هZG*] }2~ 8+dy/泗4l>bo2si[D݊b0]kiZ~>mָ.n3ץ? V:_*{ 8W&Rr|eOb>q>l8$L"_ėͯUd\꓏3<9 AUVT4sVP gaRZBբÒ*SRdSkLƮJp4}ksW)+ΨE+Tdo"uB5 v7'ɲ⶚]ՎCЄBWP#RrGJk$T쎤+_aHa_0PEl1v\RSa _B{52_y5Vc&욎 vĮ}m>bDP3_cb.^٫oȦW5{}3/V͎0~׊XTu ҂Zg4188[vO}>Z3vj>$gǞMMHkCRYREҚ~:DZY/5/V d?Uz<qCgQH>Zg*+3zqWկ9d\-]=j g{tXF&m\|߂C-Uq:.S\I>6xh饶;YI:{qq FCmZH8Xx}\k".5zT* UAhjZvS{&IP6Vj&?KT2$7I7"+pLƷU3"H3>8F"gYД+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK "  0aN0 0(  x  c $|8   `}  8  x  c $}8   ` 8  H  0޽h ? 33___PPT10i. v+D=' F = @B +d 0aN0 `0(  0O 0 # 8 0e0e ?Shape 6145"UOPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!l#drs/shapexml.xmlT]k0}?.M)m дF7IJHveJJ:܏˫MZZW6gR zLJۓ Μ'2Z\~5J\pVJ*iXȒWSI _nlIK;oUV:=ySVN[%q^O [O,+;>gJ<;]P%vxpX `| f =֚̅m܊X54ՂmJrߤ B:: \$M&xr -pkʅfʊXO+doLW PK!S drs/downrev.xmlD]K0CxodKeC@]֤$%K-xy8yr=]6RVNt2JF;%9`YҘ)'r5Ĕ@cmclʆ jr*c5f-:y!aA[9^4I˯÷ pl&Ź]os W]hU~T-N.?WeB6׳nٞ5PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!l#drs/shapexml.xmlPK-!S .drs/downrev.xmlPKD `}  8   @H 0 0޽h ? 33___PPT10i.+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK " 0aN0 -% 8u(  8 8 # p8 0e0e ?Shape 79873"_YPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!E8drs/shapexml.xmlUMO1W|&!b mEh%^{k;!l/J\rXƞg{ޛŶҺ8Zַ:;y%)e'ϟܵ gۂo,sb%r_M+5| y,mZNA7j'LoK\leGC45xwVϳ"v]87ᔖA]$LotxLWo婵~%ta/g1ħh5 Ѵ+Zk$Gxt8t7u66'09TxC6 D˝g pY %Lߝ!^?Qqy2{Kܐrꇆp}\ XמWS i[ .L%?ӋVt٣\9J~D > FUe46uI-4+euEcVP'>Xȕ4Z uƑPhF D^#dk /yW(rx|6AyqQ!3 5.&z IMS7Nq޻^`A=TXFglœy[[DxC–NՏ{\Ufͭ1U]JR'tjs^+gT]ͨ[t Td(IVILwnS$|iFsHJ9 $I00'u9'K?S7#ӵ_PK!{ drs/downrev.xmlD]k0f}vFMձ2m^b$_0<U~+9D$zr|p-tPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!E8drs/shapexml.xmlPK-!{ 9drs/downrev.xmlPKN  8  kSpec# Tool Architecture    @ 8 L@ ?TextBox 143376 w tSpec# (annotated C#) D    8 L?TextBox 14339c  i Boogie PL  D    8 R8 ?TextBox 14340"@*  jSpec# Compiler @    8 R8 ?TextBox 14342"@?) ,  h VC Generator   @    8 L@8 ?TextBox 14343 j   hFormulas  D      8 Xh8 ?TextBox 14344"@ >p  tAutomatic Theorem Prover @   B 8 n?2Straight Connector 14353"@e RB 8 s *D L 8@ c $ ?L 8 c $, H 8 0޽h ?/@8888 88 33___PPT10i.T0Y[+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +5M=>PF=)u +YPK!B?&EFR\Ǡ~of=t0] r`6*~b0+֕tJj̦ӳ$2Cp آP9|UƁH}ߣ5Ǡ5<ꑨE81,' SLLH2 eg!d&gJȶ #@zT/,&_9G"" ~S~ =E^)?PZ7V˘ٝH&pIb&\CeN#<㔞YC#uǫv,ǃ,oF S}y8 f52W]Q@w#z_Wkw8lg]iԄa Lt,ooD8?,%D j膣.<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!C 7drs/shapexml.xmlU]O0}`ub!@"@bTsu84Ա3-~N4Me\ksGONbi]mtӯI-LY뻂\ 9stIhYpm6w-vy[m$N,eCi2!KZ+ԞT d !30FGA/`}l.ܔ{/#Dn"kƫ \x liO}(W|jE$bp@պDt4+euCٮg %M]BgiA.Խ.ӵx E3@X\+³ \"-e=zb}6RXv%` W ?O|y;X3qA?W(c ɵ>oPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!C 7drs/shapexml.xmlPK-!Q7f 7drs/downrev.xmlPKK `}  8  jGoal of these Lectures    @  @ # 8 0e0e ?Shape 81922"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!٠drs/shapexml.xmlXn8/@H忤Hdw0\%*֚"$89Yh}~$e)1zhhQ@ 937?"}fWIƖZǙPKu7'YG*'H?.ꉭt)_9WOf+Q}k+aj+#s* zdTT*>fjSܰ2Oy<r¹ՂOBdm̡o1'7t,aJmN;qi_ ʭ_I0qoޚzC ;:0`<O( :om&T/zA]~sz=OxceNg`f%'nwщq 88iٽ!`nߐG#$™yY>8yeʡA*î)wLW5ZY;HAܗ " XEf!Gw~*Gd/A+9EqKc:fʬC>Zˠ$aF% 먇Fe8V9O:gm {dS+Q"ZQI\Pv%rs-.,[JArf] ȻhQ(R yJWFpuʅ:y@P3"Δl- "25,)d( S,} Ѻܵ&JGoJ)qjY~ѳC@'bH+JZȳDQqT!SBw+(UDCPdd&g@c*!'XLckb#zn&eRXpagr,}Ϭ"P`ݥxl:8k(_1ʯy t=VeJAϕ m=PK!] drs/downrev.xmlD]K0Cxoĥ]u9P&&oM-xy8y|9u $LA1}psĖ`ӓ9zWlt.&)3v%Y~b?u˧AklxQckU|쾴.x}mI~%pw ̫Y}(>>W꥙7Xx|ye?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!٠drs/shapexml.xmlPK-!] drs/downrev.xmlPK ` 8  Enable participants to Understand and verify Spec# programs Understand and verify Boogie PL programs Build your own verifier [reusing Boogie] & Zz Z  @H @ 0޽h ? 33___PPT10i.՟+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK "  0aN0 TLD(  DJ D # \  0e0e ?Shape 43009"NHPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!  (drs/shapexml.xmlT]O0}`u4|4"E6Bqhcg[J@M$^&}ιgF6:3)k}۫Μ']2Z\~6\pV6K'!oZᫌmciJ''w  i|zlzfY]|t0HGSw j%`̓>;B@25bz87pJK {yny\H*]IVl@.j^IG?E]iSlqSLU1D)I@x&>G/AADA<;lm7| #;]?"4*#On9{Y(kH=NG#qpf_{7.9N5[p3MK~Gr~8s|@ ,5dhuG%zѧ])[*^-4v 2ڟC/ZPn EF)Z1 צ(yq!ϕ;y{ե(mo_+xY\cOhBD5SL|rԍy;Q8R1ڠ* Bمœy[/ԛG"m [:;Uo巸 z: Ych_*IQV#82lwtavAKxMϺuX%qU$K|?BCRC~ j7K]N{ }PK! drs/downrev.xmlDQK0C/⒮Ulp|&zdmiso9;jCrVwȎ $2Z^_-B:BD!؂1_J(z'4(]äKdM9dQhѪM[>JϗBތgHmsIf5Nm?N g<Oߕd>('[PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!  (drs/shapexml.xmlPK-! *drs/downrev.xmlPK= `}  8   @  D #  0e0e ?Shape 43010" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!U9o% drs/shapexml.xmlWMo6 x-Wk!" QKT"Uv[K.Coӗw[|eM&R(ۢ2|wA Q4V~&Z&4I|R5wQҺ>C8 pN`p*#.QvDUdr2 RqbE<5I.! |;85p G0gpT{"󠮝+EiD{`MΥ-$4L/ޏݺ1jJwߎR[?xOa4b^baXb-& Dū9:d[Fɺg)s熜Bj@t8\1)K%[3drɀlPEwTOZ=^oiE,c g_bIdO^M]dR 4<9YFcgZ^#)!1R0e Y?~]q+c_[(ᷱwm팷*xͱ*f'ԑnV#!vRem33>ǢT3Zܟr$I•Qld2Ŝ!l1?AG[q};4cC;Ǿ-үnybW͏zzu{|pˮfϲU֫SٿVn0 A!s9Mw.hYNȔ ]Ӿe/%9n8dJ|HЪ_a.Z v> nd@o+ 2bd BS#yIpHH.Gs[-`O3OO,&@ ; r̳̉l}F"jm[4۬mK6Zh0e-uΧCP*$NP[̹⬒#co'Yl}#aKZ[Jpz7mnlE>2R1"QϞN ;G,e}kP񊸫ɷqO! {nl/tmyOW&X&h_S9M$oԘfmZI<98S:=ge"?]Q#qmn7l/-Axf@0j[U umvutYtDTRtl~ԮtZ?mזߴ4U]G7W-NRW/`gjPK!"Nb drs/downrev.xmlDQK0C/ťc+uِs['xܵ&I\뿷;ՠZv$DFW7 0QKl&jyzT^gt}Fv) R]YB71;ЏV\ZGjex6zuMGt'u>g$wg0OOi^E޷OI|=/>o?WqE߅mdΓ_PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!U9o% drs/shapexml.xmlPK-!"Nb drs/downrev.xmlPK  8  $@ 0Pp D <P kR aFrom Boogie PL To Formulas    D < [  wFrom Spec# To BoogiePL &   Xr D 0zMeXr D 07\ H D 0޽h ? 33___PPT10i.ȟ0+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK "  0aN0    (    3 4+ 0e0e ?Shape 121859"b\PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK! $..drs/shapexml.xmlT]O0}u6"E6Bgt84Ա3-~N M$^!^~s?N϶6Z ,V::R%IDƔfgϟNԶ|Mی-k8|) J!nB9rxq2GqCb3S]/Du 0pr<x_ԨGF9J wcM tOp̯K-3#RQC-nZrs Һ=K$Gd0`!39@ tIժuL+:Enw=[! \i΃SAAT.1 x`E0/ؖ/6Á BTmf՞WvX_Js |"^!5R0qṰ "ظY~00Z7uTd1r,8NEPv&kȲԫ h% =M[•[O;-=߲3F*ȶqRP!JJ_Rv t7V˺7aIvIPX<&*ݞ\S$82<H竏B:"xO7#" B 2cMKmg?PK!/ drs/downrev.xmlD[K@C8/b7i5mb[Q om4{EO{FNhE!qUi&TM᭜_f9a4L''c̙>wk_G\MN. *x[m% mMC`˖ 8%#"Q0Ѡ voIl/c.Ն=Sz~ a }9JD'V7f\>//$K򸱂<b PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-! $..drs/shapexml.xmlPK-!/ 8drs/downrev.xmlPKQ> 8  =Lecture 1 Verification Condition Generation for Boogie PL > >$ > @q  3 , 0e0e ?Shape 78849 `     +Unstructured Code Theories Theorem Provers, ,&$   @H  0޽h ? 33___PPT10i.Ck+D=' F = @B +I  0aN0 H@ (  x  c $<6   `}  7     s *6    i 6   Source language (eg. Spec#) . !&     <6  T  bBoogiePL  3    <X6  bq NFormulas    L  c $i L  c $    0\6 ba\ >      07 & LTranslate source language features using particular programming methodologyM M M    07    9Translate Boogie PL code using particular VC generation : : :    <T7   GIntermediate language for automatic verification of imperative codeH H H H  0޽h ?/@ 33___PPT10i.4Fg!+D=' F = @B +0aN0 L;(  L L # C 0e0e ?Shape 86017"RLPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!03n0&drs/shapexml.xmlTN1}ZA.\Vl VPs5z=.PUUKa3x朹o+6ҺI-L^ꇔ]9stNhrm:q5vIu8cSK ]alEGЩtR{SNvN:OdIl斕yn5U-,\xk\̌X6trKO!W 8=D5WKZ󴔔pȝKɆl%5W#m`2'ccp]Mɶg`!$sh0<([~2 z^op!kR8o/MGuB4:ΣN8{5Y0kP= HC™}YxueTAZՔ oT5jV|柕<De #.`Y6 jӀ*uiiDٮe o%]F.iA.ԭ.10@X\-³ EZ\K'(Zb}6RXgW0^7XEb|BD3ɤĂպ*+X6qʥ>ϰ: D,1Y=A\ŭE"4mk W:;Ux |2,ͨ[c(_)I񝐢uTqFy*NSZ U#!^E!m=-cĕV/  IB ڕ" ~~J^7J͞fvݯ|PK! x drs/downrev.xmlDQK0Co.cT{nw][$%k7|9薝 H#SZ՘J~}75$XX.)ۛλP0>C u]ƹ/kG#uCaٺBLklLKKDzQ? Ky{3ͽ+7I##~%a6I|t|\ |PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!03n0&drs/shapexml.xmlPK-! x .drs/downrev.xmlPKA `}  8  dBoogie PL: Parts    @e  L # R 0e0e ?Shape 86018" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!Qdrs/shapexml.xmlWn6}/ Zd}FE mca-QjTIq%=C@7Eۢd3$g.oJҺw޵9:5YlșBgB- 7U {W _x_[-.d);SI Ynl)bo2sn[̨D]r0]tPiZXXSup#cU\#v׹? ى#WK[e7j I3AZ-a#8PblrU0K}i!aQeEX*gKi 觔ɵe4*^aJ諂4Ȧ֘<]o2QizjsW(+Ψ"!P18~#'TqCAhݪ@Ny.Sm55+ <|W3k^G) uGԑA{{x =$ iTX~&|^ȸvNJ"8^(C +A' yu@Ƣ2;Q e(EZlH=Yش(ڟmSA7-i_zOr*'9(PgU_\M!RihÀwAT/7_w-g:|q?8kq`2zKz,ζR-F2"wCXzUsuq %!(#js&mqX9Pf5E8Ce;J0,(QB9|/:<ȋ/?"MzYkGMtRD,T[_WUv;%&u.a1PK!cFg drs/downrev.xmlD]K0CxoĥuԺl̉,͚|,ɶ-xy8y|9ȞѺN+$ҢS : "  0aN0 $(  r  S T`   `}  8  r  S a   `   H  0޽h ? 33___PPT10i.MxK+D=' F = @B +M0aN0 LDT(     3 o 0e0e ?Shape 101377"[UPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7drs/shapexml.xmlUMO1W| b mEMx턐_g JT*e{˫mFZWi3 HgΓH-S }tY%b.RJZ-'$wj*ˍ-hJ''8juVURͬ Բ"C2NoJ-, xLX&!2Ky šB^[k2|W#ݐMdBJr ئq`Smy<%%&Y~6͜;.BȭgnwxN!S8ܪooLԕ?hGql k`N}נz3^3jlTAZՔ o͔U%Qx18@,d'(M ƧԈ.g-47v97_G9/P7j& LZ @aAp 6g;h}k'M{?5z6R;_v{0;,hi>q>`~j!dRbj]y*jR8R<ΰ: Ḍ6YMAXŽ7g+i?Eh*txoVEXQ7Qv+I񝐢mT qFY*N]Z e#!^y.m= cĕ/Ӊ Z!܁Bf1~9T o4:%Q7QFPK! drs/downrev.xmlD_O0M5MځNBA.k٦l ?;9Qh ;"E^Wg}GXRhx|4T=ejERPzߤT]41VLZYƊD)Ujq|h^isu7x3!NO5D^?mO><Ʉ.*n[_ yܻ 6V2C PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7drs/shapexml.xmlPK-! 2drs/downrev.xmlPKJ}  6  XMotivation: Spec# s Conditional to Boogie PL,-    &     @'  Rr ?TextBox 32780x1 if (Guard) S else TN8 Z33 33B   F >   (k'  hl ? Rectangle 32770"@  yassume Guard; S& D @   (  h$ ? Rectangle 32771"@   zassume !Guard; T& D @   ZB  s *D2 >2 `2  0 N `2   0 T T  B c $  T   c $F :T   c $  T  B c $T : ZB  s *D; ;   <l x![r KSpec#     <p Bm `BoogiePL      < b &  S Then Branch       <  (?  Q Else Branch    H  0޽h ?O       33___PPT10i.+D=' F = @B +G0aN0 F>N(  +   3 t 0e0e ?Shape 101377"[UPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7drs/shapexml.xmlUMO1W| b mEMx턐_g JT*e{˫mFZWi3 HgΓH-S }tY%b.RJZ-'$wj*ˍ-hJ''8juVURͬ Բ"C2NoJ-, xLX&!2Ky šB^[k2|W#ݐMdBJr ئq`Smy<%%&Y~6͜;.BȭgnwxN!S8ܪooLԕ?hGql k`N}נz3^3jlTAZՔ o͔U%Qx18@,d'(M ƧԈ.g-47v97_G9/P7j& LZ @aAp 6g;h}k'M{?5z6R;_v{0;,hi>q>`~j!dRbj]y*jR8R<ΰ: Ḍ6YMAXŽ7g+i?Eh*txoVEXQ7Qv+I񝐢mT qFY*N]Z e#!^y.m= cĕ/Ӊ Z!܁Bf1~9T o4:%Q7QFPK! drs/downrev.xmlD_O0M5MځNBA.k٦l ?;9Qh ;"E^Wg}GXRhx|4T=ejERPzߤT]41VLZYƊD)Ujq|h^isu7x3!NO5D^?mO><Ʉ.*n[_ yܻ 6V2C PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7drs/shapexml.xmlPK-! 2drs/downrev.xmlPKJ}    XMotivation: Spec#  sWhile Loops to Boogie PLB-      &    @5  hл ? Rectangle 32769"@` E  assert Inv(x)$ D@&    e  h ? Rectangle 32770"@ `   havoc x; assume Inv(x);J DD3@D @&    ;  hD ? Rectangle 32771"@ 0p  assume !Guard(x);& D @&      h ? Rectangle 32772"@ `  $assume Guard(x); S(x) assert Inv(x) J% D@D@D3Z           t?>Straight Arrow Connector 32776"@Ex x   t?>Straight Arrow Connector 32777"@ x x    t?>Straight Arrow Connector 32779"@m ` 0m    RDF ?TextBox 32780| - >*while (Guard(x)) invariant Inv(x) { S(x) }+8 Z33  33BZ         L   c $m pm RB   s *D5    <F  8  O Loop Head      <F  8 O Loop Body      < F  P (J  O Loop Exit      <L 8j tLoop Pre- decessor &      <F x:r KSpec#     <F "+ `BoogiePL    H  0޽h ?O   33___PPT10i.+D=' F = @B + 0aN0 'T(  TR T # &8 0e0e ?Shape 9217"XRPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!u.,drs/shapexml.xmlTmk0>::iSnPB~.YnȒ')i_G`:'ݝ^N֍b+i]mtӯI-LY뇜^p<钔2OmZ_6s,IˆWJ ]elCGV:=yiT2?JjxLvj$WS2A-JcV! 'CLi w`|"~֚҅kDNbϹjioZk$Gx0:;k EД+|2SU,?<Ŝmr>8(k'( txCץqv__rgEmhGrd K`NРzHC™}xuiTAZ՜ o4-.ZW2|7J~Dy>@F ]MԪUS҈-͊m[K \ϣӌ\{5\BcK- (@X\+³ "o-.dkI՞WvvTv-x/k,hi6q>`fj!dRfbԍy;R8RXl`"fQٙ,Ö y[/+BZ{ +{<UVfM1U]/NHQV82\Ff`+_bHsM"摐w/ɪ?e˱KJHqO~ЎBRnG!\RP}T |VrJP`G^fѵ_PK!" drs/downrev.xmlDN0DHCtQ'nRRE*m< #āBB,G3sF\ zM$hBeX#+ s0X [%9`Yb”Gޟlx4 RBLQsf:.W*-z+4:-aL&D`#DOk^|>v64,.wyDxҥ:[5{ފxGQ~;Fa1vDcYPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!u.,drs/shapexml.xmlPK-!" 1drs/downrev.xmlPKG `}  F   @%  T # SF 0e0e ?Shape 9218"- ' PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!}`drs/shapexml.xmlXQo9~?k`MDJ{PI# {x=_otU(73}\׊u}r&unJeѐ3.2Zf\gMڥM7i򹬅`1W[ W{itR{qN:I{9ԢմX/eUQqEcsH!Zqc/\kc +LOp }'/5s) G8 تa*Y̙h`Ư3~NFdoEel >t]Ԕ% >vI"krdqrh`5:іg4I^jQ 78ٽVrԀz;9q>_8gf;3^]q:Ǯԍc=m6v"UO/w!)@A" X-8H ޾*Uœ񣍆Pw(WY!1>aqc}i!KEX2`FvK(QqH 9\OrVո.n=4.Jzly:<[N5\پ|'/fcDN,D$s[_(RZXUm":R}qY*K"< "4H-E^NjQaHQ~=SJI!Om+qU4p#@'įcj8 ;;ɲ%!S"k}|&boB8ܵ9 ⏾!7.& D7 ۈNyP^eKy 8P-.%t1'X p]A%mW:C쿕m(p٩vUA9:+9Qp]q"ƏWNGDC/6iafy;VKo0 +C꼺F)P Fӝ ڑ52-r׏ܬ zdRL`2 RYc&+U=Agf4yI*Xm39j߅_ hL Z:BjpiKZ[@nGC2&LjNPqWSK֢7iG;AZtA|PUx("e1w6w NۮuC EIK)Z,Eei 2{e*G | eX`^} *h M r[{ smL +^ds[nT(;$~n*fGTUҿ[`׎)¿YUAI|q`SϨ\@@A#Rμ3oxL÷ϑ'JlwfFwPK!S_/O drs/downrev.xmlD]O0MktT3Ƥnֲ 1ںM~ 9Ej5ƣ4))l7w \Y#) Ռv&- %ƧBBbJjGfviJ,VDQ.*J)0>.}V69dWOe4"q&'[omudp”vE}BxPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!}`drs/shapexml.xmlPK-!S_/O drs/downrev.xmlPK  8  @H T 0޽h ? 33___PPT10i.Jt^+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +A̋ )ѐ +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!e[Bdrs/shapexml.xmlUMO1W|YAR"g4z%^{k;!@UU)J尌=3yo>r~HJ3z̙^d3I礌׆_>:SW3j_z_IRV侚Zj c+8ER[RIxJGxLofIlyƇـ3MΖTKNx5.L&F\M:'@ B^Zkr9)H6dS//o3iwScc.¦t[psJMQ$si; S* Ϻ  :~I%lrS2s?qu2'K\sN|W%!Gu*G PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!e[Bdrs/shapexml.xmlPK-!X+ 5drs/downrev.xmlPKG `}  F  w!Verification Condition Generation" "$ "  @  ` # |F 0e0e ?Shape 93186"I C PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!;+drs/shapexml.xmlZn6}/ Zd[؈H -`:lPeH'_R hE 'd3g8#7 MdL:p˘~}zX&3&1~jl*}W1]Y[Ȥ+^2IU\B[t,%G %'bY25/3 !SA P^eQ? -S./΁XGIH'/cuv7w%J\@>HR*'W{DEfZܕMi'37($ޥz(Da%6;倎zw1Q";HQr4sz*\k)-g)XK)/mȄ4pRsҐf̀{Kd/bnPC:Vܝ,ٌi>8?k7c01> vlq >ɓZߍ CR_Cc}?9_SMo0 +Cf+ը4@rEYRv6h~Kz7_\$(RE-|lQ=nr*LߢMTNV.g}Ahzc}v-;9<L)q) !92uc:*l@PL[|9&:B"9݁|paBU@C *m4xx|6Nc܇,wu)1LZ{ &U%oKV$YgJ@1j \\2|#EhS)\CѰō?r)Eg1<T9L%{ݭP!SѩJDDŽSs*xxuLSh3ќl4ON# \!KCHQIʇi+GRGMkBߢE>'%<}v1ASLDr^ḱPK!!` drs/downrev.xmlDQK0C/Zm]6DX!Jܵ&ZWpj4;% LCnۮo`>(ҪjyyPx,C&LIhB3}ՠQ~f{[gTvjܦwBy̍jihTO V_H@7z+6I߼r)`?)] G8ak_4{`OBN<PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!;+drs/shapexml.xmlPK-!!` %drs/downrev.xmlPK8  `l F H@___PPT9" q} Passive commands: assert, assume, ; Acyclic control flow: goto (no loops) State changes: :=, havoc Loops Procedure calls | " 333333 33&>  < @8XH ` 0޽h ? 33___PPT10i.Qtpc%+D=' F = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK "  0aN0 0(  x  c $4hF   `}  F  x  c ${F   F  H  0޽h ? 33___PPT10i.5@Q?+D=' F = @B + 0aN0 \(  x  c $jF   `}  F    c $(F  `<$D0 F  H  0޽h ? 33vn___PPT10N.6B+YD"' F = @B D' = @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<*!6%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*6=%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*=U%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Uh%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*h~%(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<*%(+J  0aN0 \(  x  c $TF   `}  F    c $TF  k <$D0 F  H  0޽h ? 33___PPT10.6j+YD' F = @B Du' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%Q%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Qn%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*n{%(+ 0aN0 0(  x  c $xF   `}  F  x  c $<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!:drs/shapexml.xmlU]O0}`u(HTbTt8mcg[JB5M2iyH}9#WכR0:3Τ&+|CPxGK YBF_DW PK!, drs/downrev.xmlD_K0Co.1n *oYs675I x8guѺڐCTUS)-O/ r^!@ӓL(ΗQ`K.aj&C X-}d!u.9a1Ӳ0Q*,]w|0p[B{_Ң4}RUG*Σ-~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!:drs/shapexml.xmlPK-!, 0drs/downrev.xmlPKE }  F  oVCG 2: Acyclic Control Flow    @  S F 0e0e ?Shape 14338"   ?PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!4~.Tdrs/shapexml.xml[n6}/ ZdFE mca-ST):oK:CJbok%^47fF \g=PPb/w'dJJE?^eRseM:6&jY8 >K苔NKXK5ϸ4sQkgf-aW|}s_xĴ%% Zǹ) ()a3X\HvNv#Z9ex\$J IRsF3 OjtZFsa9uNO%("9Ș}Vcg]>5$F) aDhwΚLGvh=3'_)y d=aS" i{ayD/ +=F*Pdg*IAc] ~4-QXHt/M0 \}gW,G}zR`6dģ{6Bڸ9~)i!P̰e Sa?'2žY䰑a?4@3Zu ͕Ca, K¸w8~j< ^pR^&$Ͽ 2c'l>54a|ve] $qryexl3nO2' ۢk1DKG- (WDRmguD!_Xǀ)!.A9嘩阹[Rp+JY*w%5*+89O`b^)GD>K 6wh3XM+f6Boym?}멜7v#?VF>|T+VQ /|/nwlכW~''p2"9D]wЦc#$Η ި^FZBA\-w؎a@lde#QyXÖw;. xTP];TҰg+&2}~ZA|aW shŗ_o_OOGErEUn0 ~Aסsj9uwhENH ]Ӟe'%%nT0R] (6VVewj \C.}h;,{Q8F`4Uϯq3(KSl"ڱ{m~L+.[Ù?TNY2T J2jM8JSH&4NkR[RH<%P: W*_ [Q*#FjI fPv4E{rO{:))o)VGYA葅'W*K$d@ @ >Cn=,Kf{KzEwzM1(\Tk} H>B_B7!ز(Xu.T.V~֪ 2~)n =N\fܒx:L%)HP!C+W'Pk"⌚3 n2`r%ݶ:j3)$R6vzGB60l6ɴ;cӍ;wok?(QejO#PK!$ drs/downrev.xmlDO0M#N L Q 1~tӵmۘ/wxکѺh^uiD%|yoFtr|40]~% ΠM(ueiQog>H+تQ41Ua-*,?V_A;ȼ?|ٰ=SNOk ;~SYv|5ʛr~ ^{kkQp2N~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!4~.Tdrs/shapexml.xmlPK-!$  drs/downrev.xmlPK <$D0 8  TThe problem of redundancy wp(l0:S0; goto l1,..ln, Q) = wp(S0, wp(l1:S1, Q) & wp(ln:Sn, Q)) How can we get a linear (in size of the passive program) formula? f% % C333A@'  -  K @X  0P@#H  0޽h ? 33___PPT10.RtHW+YD~' F = @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<*h%(+('0aN0 Pl(  l l # xF 0e0e ?Shape 98305"WQPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!,T :drs/shapexml.xmlU[k0~?6צS@A(ilj,'ndɓ4'1y9sTl++Ny͙d^dș3RF˔k/ǟ?]T|KVˉ,ɝJjrcKXeIRkTh>az;f6Hv;R>4wJu[]Bdj5߄Yz0mZV3Y^+kJR6nnjV+ $GhpŐX[Gp)<,\~v9ۧ{!xJ37zN %c6>x/EvC4*#O>sd `N}נz3VxjbTAZԔ o͔W%+y< #*`%i. j[*tީ%4d~Os[_Kkӂ\-5\Bf-pAaAp ϶c;(ykq-󏶇J*kD]v?7(&S6f"*)t&%̮7eQǢ&S. @"*kMsd9ouz(q^mByaKyg-.ߪC3f֘<ʮ%)BT:);Ψ" 0[%ةwݘ+RՊ~8y$I2ϥ6S W5r8r@|<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!\ywNdrs/shapexml.xml[_o8?龃St"$BK2\;goN.{&o<'\}$j&b~IkltzHE1%[`20F|cI) /zMϋ3(h5@Ì'_(y 07攈%@=윟s=8Y(-Rc% = aԀZL%)9KLwl$٭+@XaI@{0iP+#\\,`b +(Yg/hY[߇Տn>GJe (fsa!6 X!rX0i8 -yb0elJ s !v7C]:_8KQI/e󉱮|j(*Qʏ$N?(gf@䘒k$kx2VǏ\GA@ͨpAD'{DEӵMR+ĎgndQHKu 5Fx,tFƫt|U/ EHϳQ@Nl~;|'6p֬9QdMUe ^f}u:&s%_6_,Ai@LvB2?1H=Q|7Y>}}A~+Cc]Xn0•M,DAF!D9hV %v= Hp41Ĩ1U Қ\+5HC4" 8Bp0)Ub}3Hĥ+z.8VA+)/NK˞Ap C=}6{sWX3j7=UzknΉ-$'rBa_p,BN'=LfNaWm.(]3'rc&'R8s|C' wDޓ+l'F{u !oocp|Zh ^%~]2eO# moMo俫`W;QpYF${ku)*$!Xh]5O!w0| )G fl;)ex2_9 w'8F[,4_Fl\I8M7ڒJRƷ\ziBm+].TX_UeZjS^qa#16Ya'Y3kI%Yp@^R祚t/5Fcrcyg1ryˑC ρq'h@PK!˄q drs/downrev.xmlDQO0M5H710'' 1lVz9wN7쨬 0EvO70$620]^L1D:n}z޷1./F74\Z +\֞۱J= C8?&EFR\Ǡ~of=t0] r`6*QThnw%Ig\N31SMy\|`P :}v+IgczkC;|Yq8;tk$C=_ڢ\)Hz 8޶@бpaM07Wj}0cmi!8v̵=+>mȊ6 3r0mAZIq^9OwϵRVEʙKNmv׮?Ŧv6E]Vh/kL025O*Ҿl~5$hj9ɒU̎,q[^CPK-!B<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!JC3drs/shapexml.xmlTn1W?XV F)m%<6= yMY ׾9>..7bki]at;mΤ&+<7G9O:#eL6rEvIUj9%cSI _nlIK;oUV:=ySVNZ%q^O ]O,+2韜9T*)o5qKYz=$Lt:xՌZ󼐔[؀Z0R/7)uA;qiSmy8%&Yx "sYȍgnw~Nw"ЫD5*k3#;u'c=[NJ,S5tz=qpf{f<^J9N5[p3eE~hGr~_<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!׎Cdrs/shapexml.xml[n6}/ Zd}/H -`,u} hUSJҎ!)_ dƲP!93gsy ڤJiS.#r>ߞnzd̄|H.4|HZD 1I\(1W=.-'f~[k2JzzO+E_Mܶz]J$0trN\-| $c-M!qb^$D_5i`T5Z09ZgqEI+!&_!L[ 7Cnn)ftpx`߱JtacJΎ+Cx6K"{fDhwmˋdza$v-d)WD1LGw3u~tw?Vs%TpO؞m}`37l||^]%?~m:>\e"O@v6`,7. gâΏn7PK!أ drs/downrev.xmlD]K0Cxoĥ]QmZa̚-6ojm_o99ɬW-9Ic ADbE6bG[jM//&<+B#style.visibility<*2W%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*W%(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<*E%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Ep%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +%vР3o)LuA +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!<=b4drs/shapexml.xmlUO0~ڦЈA%I(LjaJe3I׆N?:iR0j6_yߤ+Yj+ckzNjOԪްWSY ²@0q™.WHٵ.HF]M8@| ^5;yfyXI*\8˽sh W#]Gd4%α {.¦tW'd#cƓxxbT<P'dh&kC8ؚMs";m?B4*#O>q` `NРz23Zx53* -pkƅf\/eR?*q&XT#WQPT NOݡO#Bה/:^\u,hrr_p EFXl4#( 5b!<@^JŹ,>Wڳ曙׻HmY>(&QW :R fכ}Ւ fPi "dYj2Jh;P^8aީI~Ќ5LI6R-U0f;m:."լ78GB$R f;^7NUGZIw#)$ )F 0)mX\ooCPXł,!XLo; kPK!+ i drs/downrev.xmlDAO1&x1J! Deݰ}] ˿11'3Mf(Ҫtry1V'% PЦB|϶H[gTҕ\;ul rjjq^aqX ޵e6R^_u'`Zeoc'/=~/:&`:W> O~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!<=b4drs/shapexml.xmlPK-!+ i 5drs/downrev.xmlPKJ `}  Q   @  @ 3 Q 0e0e ?Shape 15362" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!;ȐIdrs/shapexml.xml[n6}/ Zd}eH[X,e*V#Q*E'v-~Iϐek4Md,,qfp4Ҟؤ {3޻.gR2Vw|{srYaZ$S2*.<9XUL򀯌'Nd*wY.ڢLRur- 0'M:nwtR+~y>T ?>4f8 8S"ż%>IYx_cYj$a*QCfͮWBKǕ˂1sNJXI ,Is-o~Ga9u jm l">_s1ɢ1g[=v Dn ~QYp [zN.Ѥq?Xq8eG-`ⷵВgS{ gzeh1u# q׀h0S5;1I 37D>_k͊0BO>!Tp<8b}~RpѭX̟Ja6nSuz2e.퐅(`*1:0[I؊,G"ga=(~+vŚu-9[:ѷkz+@HYnvXshWVYͭ'i]mIIZL4_q;<`Kuy`uYTqat|o}ܖ8HKEUe?ɟ%rmLgYdEj)}HDѯn$q "K%UZ[gCl"WU UwwQ$C[dSUbʲ]\!F"?$1)p aqHsGU(%Z?W_Ϟ\T:  Z΄X _Y r@½}k[Hr;3nu_ ݼu  Ͻjs= FKmA.R)C*ZQ/BF=;mx@QKEUJ.XhJ :.)hfG;!$ KJӮ)6(dHj ?n-N(܌n9y-L`N|Lh"L0#Ad]S7:JP/3,:}, RZ>Kk38[ ~5)Tda̴mEmD ;~RyڧZ0b[YыiY h@ѭ BУWW',CbGmyZ\̭|h@7AP7]7LKGc@ˍٷPXτ%pB+hh}Oz|vkyَL&tu 'z#OL:*/xx9H< D]ﳗ}1"9qyF°AJ,$ $I >Vy" PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!;ȐIdrs/shapexml.xmlPK-!͟  drs/downrev.xmlPK  `<$D0 Q  *@ 0PpH @ 0޽h ? 33  ___PPT10 .mԽY+YD^ ' 7 = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@f%(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<*@E%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@Eq%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@q%(+^$0aN0 j(  k  # 0Q 0e0e ?Shape 24578" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!CFJ+drs/shapexml.xmlZQO8~?iR -aHܝT-r]9--7NRJE]H%Z;;3|8|\-k"͙2Ns/W{}r/ThkTčOv aYggV+3͔Xl]*<9+}RGV*OY9L#93"}3)FUS4Z9KuCԙ:q4a`>j/f\3LiNqVP@Y&1Aωrxs=>uy06V*v?= 7?p-v{}gApHh; 岁_*M;ߟ4"Oqv0^8@} gnsdRc0Fs&m ?4L&4x+ 6 ,JJBk$l+1ߕa%C<0e"rhaLXG>F&I`EQ#HzXڭeS\ۢRULa{onȕŅvWd1[7/aɺ$uL+~q/&܇ȡ.3 *iڿfqews6 ȂܻdpZ͕/ /)K):\2D:S.b06rơB+!oc/ +ɔ.p*WfD,pJ<R[Iűm14% U1x.O͞%%o Ȝ8lkY7g$8!ASf:N;9R;"ggyQg?<Ha?<G瞅:_x.vio*[|&cE#ztukߝ|(2SlDT.U`}KD]RS,bt2)T(r|h-> "*9|׶tH7R+ɗIlj˗C퉵SMo0 +C$KŨ4۳ArEYQn΀m~L "и:QZ!MiܵAKy6wj _4Jds\,ѪAA; : `0-C }$F N`mjR{&I'tH&PIuvKr>|IZPc-]oW KSV9 }go7zOkjn+'ޭ>5x_al4B[ʗl Oۥg-]O"jc~aRIyTFW`sʤDg?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!CFJ+drs/shapexml.xmlPK-!dc gdrs/downrev.xmlPK~ P Q  "Declaration proc Find(xs: [int] int, ct: int, x: int) returns (result: int); Implementation impl Find(xs: [int] int, ct: int, x: int) returns (result: int) {& } Call call r := Find(bits, 100, true) Remark: In Boogie PL the keywords are procedure and implementation J G  E%  !% C% %  &&&        ^                          q @  # 4Q 0e0e ?Shape 24579"VPPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!~G+drs/shapexml.xmlT]O0}`uR"6Bqhcg[JILZkks?/bi]itʻ'I-L^ꇔ]8stNhrm:q5Y:Kqb)+rǦ؊N`rN) ?BdΞ!?8 ȭgQ7@@?="kD :+? #;M?"4*#O8{5Y(kH="R̾,xr -pkʅfLghGr>J~Ds#*`Y6jӐ*uiidٮU o%]B.Ђ\-[7"G#Z.j1mvQ /%:Jcez멲w(b^kxY`Oфs : eW몬cو )>hz4&d朆Xr^-VBċPmT(/l0T204on)*?U=uTCqFy،*N\ Q£ onE!붞VuxcđV/wICwڑ$~~!O(|K|N,[G7 atPK!<: drs/downrev.xmlD]K0Cyo%SlUM6oJ_o99f]4(  +v *h`XX&jH}X0cB\Q+- WVDZq lݑh`Ev*K3-%2u|J6cj>BÜoyU&^!?ۮ_A2b|m#ἲ (PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!~G+drs/shapexml.xmlPK-!<: /drs/downrev.xmlPKE `}  Q  iBoogie PL: Procedures    @X  0X  0 X  0 p H  0޽h ? 33___PPT10i.0kb+D=' 7 = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +JwN`(x" %H' +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!" Q-drs/shapexml.xmlZn6}/ Zd}/eH[Xs@T"Uv<%=CJvlش^囹eH팆d߯3Vokr&ulfۛ3 'L(eĵ/~<9X] ϝˇFe&w&}pFne!dn6{F&R/0^MRa5,Eia\QS7J0DEɎx ;3+ 'L-iaUs=^^ZkR j bŭM>g1S3{`N{A1VK-fq.&I-Cǜ=^Ie0/rXv{vbPt:Yh^|WFtN!9'΋ߗJԯ:0|™}3qڨc1fd&˅ICU{Tp6+ R+eŽ"~ !ˣVATTBLntT* c+.(H@.1|x/uEZ$tEBرp<'>)|nC)ۧ ];]^+{j.'O $T> (y'"qlQ|%Q1b- A lwHSH4U8.|g ia%4E>>_|TR olI|ܵC,*MܤJBKaT:F7 q`.M-FWL2Id*-G뒖*Q|pKD ~re0{R A`]gOYWW=O zc3(1mUI]G*Tn&hHS9b,8#ⳳQ dn( +g3P+S JلQv̞SUC&5_@ "v0?.WL MxXBḨ1T!+euJP oUg{($=TEQj"G<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!9drs/shapexml.xmlUMO1W|`YAD[)Bs5%^{k;!ٻ|EUU)J尌=3yo>rv[K*3?q&0E2~w}pʙ RFˌk'?5k|K/o$qb!krؚ +˜t2?b2w +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!rF#y$drs/shapexml.xmlWmk9~pA둮c;/6ٔ$SL~]mVJ3ڵ];R ]c֒f$<3b/I點d6/S*?=ܟ\J5*׿vU}-qE8I|PwVº) I;OIE8̬g(:Q.) UwZ ^ˤk,l[s[=#K:s[݂̓q>/垗qsMZk`,[S/Dxa/oR9쏆(〽>zMM᪷}Ec[.O{=fxM2h gA4%W^niqqUgGYSR hdxv}-H:P"Txfꬍ]hnK P0HQ lH f?zUʓ'"Wg-h Th([\Xn9yhZ1p+S$bxl&YRrqc]Ng5npGBWw=l"u7+RT 4@aB*+lשT ,b)Qب H8b"\Òa+Ns]2FY[ıVa᧱֍͊y14NiE^пD)2G@NREm51-+LVP̉-Б@Q# - C~|| < gTQ&#6@~d~@o nLj{6qcwm?eTW\FW\蚉}[3I?q}.4A݀Ybv~@%ާ\>RH hS6,@ ɢWh?\Ng370NٔEB{8tf4eC{b:,OBWplu'XZ,xul.m~zm?lKޭvwLO pPRŽ$t\{bYnSa N,ʒ/r(0]v2x3Bw|5=!pMk3"^z*5/?-}q$Ʊ@&CRKn|d?PK! drs/downrev.xmlDN0M|7@3sBLDAQ{umaw11\}g:tC ("4ƊA0LQƠdˋ)τi1mH@q*QK%5#c%8C]Em DQBcyV+Y~oMi+r*]_u; Av<q>6_7U' n'1">H :PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!rF#y$drs/shapexml.xmlPK-! @drs/downrev.xmlPKU `0  d  Tvar xs: [int] int; var ct: int; proc Find(x: int) returns (result: int); requires cte"0; ensures result e" 0 result < ct xs[result]=x; ensures result < 0 ! ($ i:int :: 0d"i i<ct xs[i] == x); impl Find(x: int) returns (result: int) { start: ct := 0; result := -1; return; }| U%  " "        $$(((( ((,",004488<< "&&"  "  &  "  &  "                  ?   $             . @  # -d 0e0e ?Shape 30723"ZTPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!n)8drs/shapexml.xmlUj1}/^Kkx:$LgJ;_Q%Y8VcW"vM87d W 8j&+KyeyZI\8˭KhW#]Q4vGgcm]n/(1ygCsʻwbD<PwA t:^%c6s^٩~ Ѩ8<8w?7dA#87 gfAĨÃ))+S=D=Js "/MpXT+N#wQPT3NO-ѧ]&{Z [o}m/i:rnN r_np EFm4#( Ub&<@^Kŵm_* oګ.6ewfousQM<-Gl,DTpSLJ,]oʢ4EM*\꓇9FCET&04r8Ql--EX‘N{-nߪC3f֘<ʮ%)BT:JgT[njEP<&R6S O5r8r@| +pAmA;8y +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!3$drs/shapexml.xmlWn6;YĎc#" QKT"Uv}>ZIɉ=dMg8fl--Jx]3R6oN9TFR+p8Fb8J¹jjt!Jt%d6%9Veʑ=luqBsSi51~Vd ? zwJ0u[^a1Z&7H9{}n58B~Y ^7/!\5rKDO萝CF9I sNJL9^B,+-RXMCdȍմJHZ7uRB@iXIfGCGc\> ?j4Hޢa%goh>}AaAcuisE82'aF'Z#JqI= lBk}A;غ |?L Vwkp iUY" &\Sp&q:pQe T~L t: +Ζ HE껡-T3( A61ZamKw%;9SB@ܱZ<K"EVcUCWPw+sJO:..hO ( R'H !HlE|`w6(8&dIR>xQ|׷<= ;Ex{?.KydҧG}ބZ"Tt> <-|-q^~>Dg(a*_4|nsVb.%ӿ͊\M){+Ȇ&8`_htOIJTAA+OY .sHF4n C[2b#͚_{du5޲ LP߾{#JEmI>͙Bg̷+.r9LFu}Pw*/A?#I3~.N_Try yC6w92[tPK!9 drs/downrev.xmlDN@E&3qC`ZkhS1)3gRƄ;[%ъA8 Uhިc=N8c`4,W3L>Lt_\ jMJ+j!MjJm%!ڊr-[zSQ.j4G20ӝWѷ0]nFㆱۛ~ċ*f—}.3>R>?m3t^X/PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!3$drs/shapexml.xmlPK-!9 Pdrs/downrev.xmlPKf   H$@0 d  JPostconditions often relate pre-state and post-state ensures x == old(x)+1; must say which variables x might change modifies x; variables not mentioned are not allowed to change proc Find(x: int) returns (result: int); & modifies ct; // would allow the previous implementation ensures ct == old(ct); // would disallow the change (despite // modifies clause) % Z&$ Z$ Z($ Z$ Z4% Z Z% Z&3(34 + \t      a  a @  # |d 0e0e ?Shape 31747"]WPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!E:drs/shapexml.xmlUMO1W|h!bR"g4&KvBٻKUU)J=;|l[+UFgn"[MNեQi[3.6S7zވ.{*IAD>wMXTN#7QPT NO-Ч]![[o}k/i/*ri?N9/ZPwj"G#ZaAp 6kKG]%U{^?u|}6R/`l1||BDw=ΤԂպjPqƥ>c=Tȣ5Y9AZũ7g+i?E(*twz604nf)j${BJUJ@{〉py U6~;",78GB$R m=T'*#$_BZpu#I߇e,!mRbF,yG^o DL~PK!' drs/downrev.xmlDMO@&5&*iǥ6~dw߻11'3LfeѺF+BԢQ.K r+;ҰZ^_-x*Ex* RΠޤFHT;i+VDX~ lّ1S2!7*LSe zK D Ư.Hc axl纝MM}W6N_"L}xtzw- dPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!E:drs/shapexml.xmlPK-!' 7drs/downrev.xmlPKL `}  d  mMore about Postconditions    @  0q ,$D0H  0޽h ? 33___PPT10.0Pm+z Dv' d = @B D1' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Mu%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*u%(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<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*/%(+PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +wK͋s*?&EFR\Ǡ~of=t0] r`6*i2)/&w7qR >5}ϝ{]ONJIXUB%\:H/(TƤVp4t,Xާ$R"7Zf~shMF2s9\mwk|vju zg"SGH] ;Xݺ^euxwՅ:KfmBYt7wfB,R*K(~}&Q2y۵E ZC-=OM;kcеq;ޢ9dp)x5,Et?>:8 n| mi˕?vp+uN;x5+yML򽩰b$ b :S@? /"y~lq9VtWwbaR 8Z28:ek8K&7;D9 r(^|?H/ˊ_xn3-->-`gJjo{\!JlL|@?cO*Eʇz +gOGz%t^k`Y@ݣNE3-9%׸J:U= O7Ѥ5}&8D'B}_PK-!B<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!+drs/shapexml.xmlTMk1%vx:$LˬVo}nL)\ a=h8=֊muOI-LQ^p<邔2OM_&Ksb)krؚL:/u60=Ԕ% A2gGIȁRL@}2LA/`$aM%lskR0.xGuںhtG}8w?dA$3VxuiTAZՌ o ^4)q!Xt"7QPT NOcN#B/:^L_Ulhrr_p MA@aAp 6g4Ks'U{^?u|}6RO/`||BDw3ɤԂպjPqƥ>[`=tȣ5Y=AZŭg+i?Eh*twz1𭪰4nn)j$wBJ6WR-U2v;m9vkEYo*Wq0{ILwCN]WZIw+Zp{ ẕ" ~~Nh|JbNPZG^o׽5_PK!> D -Ek4q뫙ȤuNWQ`h ]ʚp#ӑX%|BiEت1c豦XGM\r~{3,y%|ڽv)Wtl{,9$$O?{\8OPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!+drs/shapexml.xmlPK-!>+B#style.visibility<*OT%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Tm%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*m%(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<*N%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +:7׎ d!K4ķcz +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!+drs/shapexml.xmlTMk1%vx:$LˬVo}nL)\ a=h8=֊muOI-LQ^p<邔2OM_&Ksb)krؚL:/u60=Ԕ% A2gGIȁRL@}2LA/`$aM%lskR0.xGuںhtG}8w?dA$3VxuiTAZՌ o ^4)q!Xt"7QPT NOcN#B/:^L_Ulhrr_p MA@aAp 6g4Ks'U{^?u|}6RO/`||BDw3ɤԂպjPqƥ>[`=tȣ5Y=AZŭg+i?Eh*twz1𭪰4nn)j$wBJ6WR-U2v;m9vkEYo*Wq0{ILwCN]WZIw+Zp{ ẕ" ~~Nh|JbNPZG^o׽5_PK!> D -Ek4q뫙ȤuNWQ`h ]ʚp#ӑX%|BiEت1c豦XGM\r~{3,y%|ڽv)Wtl{,9$$O?{\8OPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!+drs/shapexml.xmlPK-!>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*tF%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*tF%(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%(+\"0aN0 >6 (    3 T.0e0e ?Shape 47105"b\PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!c/cHdrs/shapexml.xmlUj1}/^KK;^I mMX7J[Iv}(mЗA;Hs\|vHJSLjaR/R~w}tʙsRF˔k'?Չ|K/Nlj}6V䱵Nmړ;aSQMVlffY|0uinZpt;]Bdjʵ߄[zw0mXUs$֚ǥ܅c܉!6DS//o?8 : \Mɶ&g`H)`x|Dn=Pa z.6^JV'~{i=i~Ѩ8<8w?dA7 87 gfFՕQ)i[S.6S:E=JRp}@F U*ӈmԦUS iDٮe o%M]B.iN.ԭ.xfE Z̄gµ=s{}%E{QصJٻmvv5`-Ec4r6ۛtmJ28*S ccQ]aa҉npN)UE%,>Wošw̲ʓh~49p~'O@|c-**}LWqbw9ZtPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!c/cHdrs/shapexml.xmlPK-!d9 <drs/downrev.xmlPKQ}   BoogiePL: Arrays and Background $   @  3 h0e0e ?Shape 47106" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!;[lg#drs/shapexml.xmlXn6}/ Zd-_⬍(@Fa%QjTIqO %YcXuCqsf(J6bki]at̻"ΤNMVE?=_y31׆j*ڍ/ƝK-7vѩtR{N:(vR`2W3K̲"]qEuKQIF]Ci!H&]8O gpXLB/䭵i)E+w-Z Z2\gbgUotَk1>ZMn\sF_^cΞ{Ex1Rz#scpٻ f%ـ~sh4Euݏ!硓/=Y3գ`p>܄X8-&F#N1k="3e%TϫNs!6%pD+NcGҐ*Q&Bg(_l=Z`gD2iI`1RL]|΍aH"ьJԭC(QZXW5\Rv#Lyq'C_$s=ns軝~5' iWiMOj)jFngI&`cwB,OgS&^$S78hbZ, VuY \OsУ*0 ƥ T~m <8[I =!EJzQKFK%UAqͬ1yhOabNiP qFuz"ّE#?&㋉doievHU"E?Bs) R4RG aQ򊺩D:NJ% yu%u"GIAO-qM&cPNVMxأbz%<蠇God: +~ubR}oOۍ쟼=a(OOWN0 (WpbZ'A%aYIhۉodIpaT!rluފY QZ*D`2Wծls墛F"y5'5(;Dظx(e;^,%/Gv1Sƿ?( #8sRvpl6uckʟ)ӌK}:̯2~{I2KqmDsp\j%)n*m\^ɧ,KUk|kS8c(&JBCPfmkUOHIf嶸&MM @#pKoZ BYXZY \4RTs  Ax2iq 0do)n9Կ:V'uӱ;tDd/.nq4L]lkO#2t.'D*{Ci6-fPK!`D drs/downrev.xmlDJ@a97nb"V[4fO~0{6irYݲk 0¨*qs3$%[C(  (sWltK.5j馦CX-mŕѭ[~3q-/j#S]%~n'|+d)jS~ezymY V>mR+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*J%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+Q0aN0 Pt(    # L@0e0e ?Shape 109569"\VPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!rf=drs/shapexml.xmlU]k0}?6M)m PF7IJHv JJ:܏_l+6ҺI-L^Eo8stNhrm:q5Y:Kqb)+rǦ؊z0ܠ* Ḅ YI!\ŹE"m [:LC*6WJh uCNRٺWIk6qBa+JT_N3,5?tޔ>Dß{S,\ѮN&t_3]KW9 PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!rf=drs/shapexml.xmlPK-!e 4drs/downrev.xmlPKK}   hBoogie PL: Final VCG    @.  # ċ0e0e ?Shape 109570" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!κ1drs/shapexml.xmlZn8/@p8(E bQgXkRtw7G'7;|(ΐGCgbfq&uhF~9gz$2rva:iΥj5 2;J Zdl"^C52 uUmjgՓj"b/1~=KǞeV3-,T2WՂ3$ KׄHFOPrC hYs3A^YkR2U/\^ qIts Af̡,্ih7q93&XyEgdw//DDś-3>ը EG A?o4,ilx1sYpiͮ&` s/=Y̳JP맧 gv2\8ucT1BA3uu? ۉ\=+ y '`݀i*xQ^!^sUdt/4 .#EW_ۉhw EF0#uAuCoC,RGT+BYBWx*ǵ6yt V̱上&|JFy8,Pe(,#}7q'cϢY(ӪWxjjX6P.yEeQV߷76生juZ^Y%ޔ@Mv72CLIxXߤ~=j< }4qYD 61~Rv~,^ʢZs-Ύ8) tsE` U}hzr(ho֠ŝ*Pm ʽlk*H.߯q7t{--?a*^tCPgVMk0 +uV=Pv.^9h珮 A֓gTx;Aa%Z.J;!E`]ژby]n~c1gHhn͗X $r*4&9d_I6V7ج%ESթbc[ }yn!i遞S'۵~F'~'q|yD mtFة8#+*YFF A?:jrCu/O=/xFX[\’Vq*#e ՜ PWëPK!79 drs/downrev.xmlD]K0CxodKnu(Sq0[ûؼ`M%qkaxy8<3[t!6hȀ΍ua8q^h)6D,Qx|ICXpocJ]^nhZ+UiK*8j5cJ:LTe.VvIѼ&~?uxr~y%w@>zy&~%A6ߎOe*GˁPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!κ1drs/shapexml.xmlPK-!79 drs/downrev.xmlPK    LBoogie PL has a universal background predicate BPUniv Each Boogie PL program has a local theory BPProg The generated VC for each procedure implementation P is: BPUniv BPProg valid(P)  / * ;     /  ,  =       @X  0` 0@ H  0޽h ? 33___PPT10i.ԋ.+D=' = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK " #!0aN0 `/(    # ܋0e0e ?Shape 39961"c]PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!c Gdrs/shapexml.xmlUO0~ҖRhDۤ UPlI)i!9MZZWgR !wGg9O:'e̸6byW:M'"RCW[>$NjOT*u:8|zVOmzjYgx88TقjV']Bdbҵ߄[z70mXV3^~֚܅mܜjokK$G{pp5N8u6V0:~tn!=r㙀~0<;w93〯%mS26xEzĿiGqd +N}zi R3jlTaDZԌ oT5բM*~}@,ʀUd'(u9Ш].;v-[!K+ YaNsr_np UN]t#( b*<[vӖK+Yݛ,oZ|5Vnfg07E||BDM֤Ԃ*+X6qƥ>a=Gec N,mco%Ζ҂؋PU(/l0T_205nj)*?V9!D[R@*y U&~Ӌ"U/8GB^$B m5-pU+*3 #Bopoµ$ ~ľƞ彴V^RS)aD;އ_DW~PK!]u drs/downrev.xmlD]k0FfRY:>.F[k$%4+9s˨;rF[k$cMeUkj~{wiArq}5Syj28O&>W jǶG3tG Ct5UN^脱R-[3\4uiDzOTzL^}S^ۛz0z42y+,Wѕ/ ?WL9MUtPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!c Gdrs/shapexml.xmlPK-!]u =drs/downrev.xmlPKR`   %Background: Automatic Theorem Provers& %$&    @  # `0e0e ?Shape 39962" PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!pRS/drs/shapexml.xmlYn6}/ Zd}/eH[XsAT"UvT?lFsδȰl)rɨ[\"īTG|: +a&L-`UsA^[kR, j-bMd)sxP^w Q1Z^ե$aX| p(Cy1[bp Đ:mTAogP. dq~2G+yZXəUrWza3q֨CHF2M,K߉*=)z<^ `|pc RB M2J/JҧZc_.2wJST`@h)Jq,+Nw /EhꐓjH+ݙdU'uMKe(>%"?eL2)BG\tE\]hc?"PÜS|}ns̩h5iAF)A}a)ЦMC ֎Ùꮡhq;Gq aYs\"|T.ϡH N|spW `Lu-^ "gVn0~k*v"!J$Q6cHPTx; $=]YH~x}t3NWv v[ۼe|ʗא*,LTy/.:y X=t JG n{:pjٯ?З -88XLrӹ֢mɭ_&l߷Տ2į( (8 g5ur/g{a1 +0#Ta mAɣ%$v:unnߵns=zV*3V~vDTL;́2;SS,xFC" K k|4Z] 9g$ AYx. 6-$Ŷ*T}M$-H D&Wx] Y=I'oWjK+H1Pt>[P.! ބ->j:WSt.s97|bG$&uYPK!V drs/downrev.xmlDQK0C/ҭlu'5YSmn$n[pf0-;+Kʆj~$%%,lW+LPe Br+ :aetϢ(17xSOZU%@q^b߽r!no`A |Z!hg>/r[?W,e;mPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!pRS/drs/shapexml.xmlPK-!V pdrs/downrev.xmlPK  @  Usable ATPs have to support first order logic examples: Simplify, Zap, SMT solvers They are build on Nelson-Oppen cooperating decision procedures and have decision procedures for congruence closure linear arithmetic partial orders quantifiers Their key features are automatic: no user interaction refutation based: searches for counterexamples heuristics tuned for program checking Labels and time limit. Z& Z` ZA Z Z Z.&`A @  b  & @H  0޽h ? 33___PPT10i.T0Y[+D=' d = @B +PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK +0ي16-$i9Lgs +PK!B?&EFR\Ǡ~of=t0] r`6*<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @  S p 0e0e ?Shape 40961S"  `  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %  @ (  W  3 (0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @  S  70e0e ?Shape 40961S"  `  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %  P (  W  3 l7 0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @  S L0e0e ?Shape 40961S"  ` 7  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %  ` (  W  3 7 0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP}    @  S `0e0e ?Shape 40961S"  ` 7  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %  p (  W  3 8h0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @  S 0e0e ?Shape 40961S"  `  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %   (  W  3 L0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @  S 0e0e ?Shape 40961S"  `  @H  0޽h ? 33___PPT10i.ȟu+D=' d = @B +&  0aN0 %    (   W   3 T0e0e ?Shape 35841"a[PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!8g?drs/shapexml.xmlUN1}Z%+6h+E("&dN.QVBKy،=c{93l-xÙP.*5)g֑*Hj%24?}t֤a8ld|\&&{+aiIcʑ;LzqOj26f=1*2?:8STV'm\[@^Jmĥ(cwދ&VWmtb^S(8 &ظඝД0\UH*g\)؋}0 #N,L o,Ζ€7h(_^R~j+[V~^h]J _+)#c xcU(V$B0}x M,EvƪujP%a@vОCPtvϑv@Cc,Řo8#T1!CO2BGrLی~PK!V[ drs/downrev.xmlDQO0M5M 5lRDP@cY/dmg[.&Ǔs Թ.8l7煖69hXҴ:c ;&%*Aw{c}V[4d/J~)e T ]BgϺ /?8͞,3qڭQ0]@;[D8:PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!8g?drs/shapexml.xmlPK-!V[ :drs/downrev.xmlPKP `}    @   S Tw7 0e0e ?Shape 40961S"  `  @H   0޽h ? 33___PPT10i.ȟu+D=' d = @B +r 0yWV 08X7g VٛM;&PFC h"- =2OTqup `9e~v "V[WZq|s~>lȶX1Oh+'00 hp    (00Towards a Verifying Compiler The Spec# Approachschulteschulte197Microsoft Office PowerPoint@ӡ@r2@pGg  9  y--$xx--'"Arial Unicode MS-.  2 q1."System-"Arial Unicode MS-. 3f32 0Towards a Verifying Compiler:.-"Arial Unicode MS-. 3f"2 ;&The Spec# Approach.-"Arial Unicode MS-. 2 J<Wolfram Schulte.-"Arial Unicode MS-. "2 R8Microsoft Research.-"Arial Unicode MS-. $2 Z5Formal Methods 2006).-"Arial Unicode MS-. 2 kJoint work with .-"Arial Unicode MS-. .2 k-Rustan Leino, Mike Barnett.-"Arial Unicode MS-. 2 kS , Manuel k.-"Arial Unicode MS-.  2 k`F.-"Arial Unicode MS-.  2 kba.-"Arial Unicode MS-. 2 kdhndrich.-"Arial Unicode MS-. !2 kn, Herman Venter, 0.-"Arial Unicode MS-.  2 oRob .-"Arial Unicode MS-. 2 o DeLine.-"Arial Unicode MS-. 92 o*!, Wolfram Schulte (all MSR), and .-"Arial Unicode MS-. 2 oXPeter .-"Arial Unicode MS-.  2 o`M.-"Arial Unicode MS-.  2 ocu.-"Arial Unicode MS-.  2 oeller.-"Arial Unicode MS-. 2 oj(ETH), .-"Arial Unicode MS-. 2 ot Bart Jacobs.-"Arial Unicode MS-. 2 r-(KU Leuven) and .-"Arial Unicode MS-.  2 rFBor.-"Arial Unicode MS-.  2 rK-.-"Arial Unicode MS-.  2 rLYuh.-"Arial Unicode MS-. '2 rSEvan Chung (Berkley) .-Root EntrydO)VEY Current UserDSummaryInformation(b`PowerPoint Document(.      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`acdefghijkpsuvwxyz{qr - "#$&'(*+,./02456ttDocumentLibraryFormDocumentLibraryFormDocumentLibraryForm This value indicates the number of saves or revisions. The application is responsible for updati  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~tomXml"/>w>      DEFGHIJKLMNOPPublishingExpirationDatePublishingStartDate 2018-12-08T06:59:54Z2000-01-01T00:00:00Z ng this value after each revision. .DocumentSummaryInformation8lRoot EntrydO)/Current UsertSummaryInformation(b`PowerPoint Document(. ՜.+,D՜.+,H    On-screen ShowMicrosoft Corporation.d*d 1ArialArial Unicode MSCalibriSymbol WingdingsHGPSoeiKakupoptaiDefault Design1Towards a Verifying Compiler: The Spec# ApproachThe Verifying Compiler(Spec# Approach for a Verifying CompilerSpec#: Research Challenge Demo (Spec#)Spec# Tool ArchitectureGoal of these Lectures Lectures>Lecture 1 Verification Condition Generation for Boogie PL Boogie PLBoogie PL: PartsLimits of Boogie PL -Motivation: Spec#s Conditional to Boogie PL-Motivation: Spec# sWhile Loops to Boogie PLBoogie PL: CodeBoogie PL: Meaning of Code"Verification Condition GenerationVCG 1: Passive CommandsVCG 1: ExamplesVCG 1: Assume-Assert Reasoning/VCG 1: Correctness for Procedures (simplified)VCG 2: Acyclic Control FlowVCG 2: Acyclic Control FlowVCG 3: State Changes VCG 4: LoopsBoogie PL: Procedures$Boogie PL: Procedure SpecificationsA Bogus Implementation?More about Postconditions VCG 5: CallsVCG 5: Bodies BoogiePL: Arrays and BackgroundBoogie PL: Final VCG&Background: Automatic Theorem ProversSummaryAppendix: VCG ExampleCreate assume=Move loop invariant into Loop-Pre-Header and after Loop BodyTCut back jumps: assume havoc on variables assigned inside the loop;block loop body &Create Dynamic Single Assignment FormPassify AssigmentsApply Block Translation and wp  Fonts UsedDesign Template Slide Titles*4 $, DocumentSummaryInformation8MsoDataStoreVEYVEYONCQUENGA==2 VEYVEYItem !