%PDF-1.4 % 8 0 obj << /S /GoTo /D (Outline0.1) >> endobj 11 0 obj (Java Card DL) endobj 12 0 obj << /S /GoTo /D (Outline0.2) >> endobj 15 0 obj (Sequent Calculus) endobj 16 0 obj << /S /GoTo /D (Outline0.3) >> endobj 19 0 obj (Rules for Programs: Symbolic Execution) endobj 20 0 obj << /S /GoTo /D (Outline0.4) >> endobj 23 0 obj (A Calculus for 100\045 Java Card) endobj 24 0 obj << /S /GoTo /D (Outline0.5) >> endobj 27 0 obj (Loop Invariants) endobj 28 0 obj << /S /GoTo /D (Outline0.5.1.85) >> endobj 31 0 obj (Basic Invariant Rule) endobj 32 0 obj << /S /GoTo /D [33 0 R /Fit ] >> endobj 38 0 obj << /Length 1004 /Filter /FlateDecode >> stream xڽv6ί<"7;iLr{`hZb%_@H)=鉘̆ـDp&/WC~\ L 11J14Tm"byb}@ ^!GsB6W"4GbA)jQaIҠHb 3؉1DQ1e0Ys.r1 ,S k8VL*n/1*6ɘ+V.?RW> R S&Wtv@6TCx\ eV:ުO|=)l@2b%yl%8h\~Uy;[|k͓,eLyhqJV 5Q7V1xuT6(Sp0NFwn$gێH'^3JA3ڠ$ W_Gα>/7H-sIb<_"QdkoVeS "MJWXJl?H +W`Q̈́cn3ȍgV}66Ja