%PDF-1.4
%
1 0 obj
<<
/PageMode /UseThumbs
/Outlines 2 0 R
/Metadata 3 0 R
/Pages 4 0 R
/PageLayout /SinglePage
/OpenAction 5 0 R
/Type /Catalog
/PageLabels 6 0 R
/OutputIntents [7 0 R]
>>
endobj
8 0 obj
<<
/CreationDate (D:20090601123154+03'00')
/Author <426172746972612044616E7461733B2044617669642044E968617262653B205374657068656E736F6E2047616C76E36F3B20416E616D61726961204D617274696E73204D6F72656972613B2056616CE972696F204D65646569726F73204AFA6E696F72>
/Creator (Elsevier)
/Producer (VTeX PDF Formatter 1.0 \(Windows\))
/AuthoritativeDomain#5B1#5D (sciencedirect.com)
/AuthoritativeDomain#5B2#5D (elsevier.com)
/ModDate (D:20090616141643+03'00')
/Title (Verified Compilation and the B Method: A Proposal and a First Appraisal)
/Trapped /False
/rgid (PB:222138868_AS:103010113949699@1401570934260)
>>
endobj
2 0 obj
<<
/First 9 0 R
/Count 6
/Last 10 0 R
/Type /Outlines
>>
endobj
3 0 obj
<<
/Length 6266
/Subtype /XML
/Type /Metadata
>>
stream
application/pdf
doi:10.1016/j.entcs.2009.05.046
Verified Compilation and the B Method: A Proposal and a First Appraisal
Bartira Dantas; David Déharbe; Stephenson Galvão; Anamaria Martins Moreira; Valério Medeiros Júnior
Verifying compiler
B method
Elsevier B.V.
journal
Electronic Notes in Theoretical Computer Science
Copyright ©2009 Elsevier B.V. All rights reserved.
1571-0661
240
79-96
79
96
10.1016/j.entcs.2009.05.046
http://dx.doi.org/10.1016/j.entcs.2009.05.046
2009-07-02
2 July 2009
C
Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008)
Elsevier
2009-06-01T12:31:54+03:00
2009-06-16T14:16:43+03:00
2009-06-16T14:16:43+03:00
True
VTeX PDF Formatter 1.0 (Windows)
False
uuid:63038AF68E4EDE11AF05CC2DBB82D44B
uuid:7cc5110a-cc48-4c8f-831a-bfc3a534ec55
1
B
sciencedirect.com
elsevier.com
endstream
endobj
4 0 obj
<<
/Count 19
/Type /Pages
/Kids [11 0 R 12 0 R]
>>
endobj
5 0 obj
<<
/D [13 0 R /FitH 680]
/S /GoTo
>>
endobj
6 0 obj
<<
/Nums [0 14 0 R]
>>
endobj
7 0 obj
<<
/Info (sRGB IEC61966-2.1)
/S /GTS_PDFA1
/OutputConditionIdentifier (sRGB IEC61966-2.1)
/DestOutputProfile 15 0 R
/Type /OutputIntent
>>
endobj
9 0 obj
<<
/Parent 2 0 R
/A 16 0 R
/Next 17 0 R
/Title (Introduction)
>>
endobj
10 0 obj
<<
/Parent 2 0 R
/A 18 0 R
/Prev 19 0 R
/Title (References)
>>
endobj
11 0 obj
<<
/Parent 4 0 R
/Count 11
/Type /Pages
/Kids [20 0 R 13 0 R 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R 28 0 R
29 0 R]
>>
endobj
12 0 obj
<<
/Parent 4 0 R
/Count 8
/Type /Pages
/Kids [30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R]
>>
endobj
13 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [38 0 R 39 0 R 40 0 R 41 0 R 42 0 R 43 0 R 44 0 R 45 0 R]
/Parent 11 0 R
/Contents 46 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 47 0 R
/Resources <<
/XObject <<
/Im0 48 0 R
/Im1 49 0 R
/Im2 50 0 R
>>
/Font <<
/T1_0 51 0 R
/T1_1 52 0 R
/T1_2 53 0 R
/T1_3 54 0 R
/T1_4 55 0 R
/T1_5 56 0 R
/T1_6 57 0 R
/T1_7 58 0 R
/T1_8 59 0 R
/T1_9 60 0 R
>>
/ProcSet [/PDF /Text /ImageB]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
/GS2 63 0 R
>>
>>
/Type /Page
>>
endobj
14 0 obj
<<
/St 79
/S /D
>>
endobj
15 0 obj
<<
/Length 2574
/Filter /FlateDecode
/N 3
>>
stream
HyTSwoɞc
[5laQIBHADED2mtFOE.c}088GNg9w߽ '0 ֠Jb
2y.-;!KZ ^i"L0-
@8(r;q7Ly&Qq4j|9
V)gB0iW8#8wթ8_٥ʨQQj@&A)/g>'K t;\
ӥ$պFZUn(4T%)뫔0C&Zi8bxEB;Pӓ̹Aom?W=
x- [ 0}y)7ta>jT7@tܛ`q2ʀ&6ZLĄ?_yxg)˔zçLU*uSkSeO4?c. R
߁-25 S>ӣVd`rn~Y&+`;A4 A9 =-tl`;~p Gp| [`L`< "AYA+Cb(R, *T2B-
ꇆnQt}MA0alSx k&^>0|>_',G!"F$H:R!zFQd?r9\A&GrQhE]a4zBgE#H *B=0HIpp0MxJ$D1D, VĭKĻYdE"EI2EBGt4MzNr!YK ?%_(0J:EAiQ(()ӔWT6U@P+!~mDeԴ!hӦh/']B/ҏӿ?a0nhF!X8܌kc&5S6lIa2cKMA!E#ƒdV(kel
}}Cq9
N')].uJr
wG xR^[oƜchg`>b$*~ :Eb~,m,-ݖ,Y¬*6X[ݱF=3뭷Y~dó tizf6~`{v.Ng#{}}jc1X6fm;'_9 r:8q:˜O:ϸ8uJqnv=MmR 4
n3ܣkGݯz=[==<=GTB(/S,]6*-W:#7*e^YDY}UjAyT`#D="b{ų+ʯ:!kJ4Gmt}uC%K7YVfFY.=b?SƕƩȺy
چk5%4m7lqlioZlG+Zzmzy]?uuw|"űNwW&e֥ﺱ*|j5kyݭǯg^ykEklD_p߶7Dmo꿻1ml{Mś
nLl<9O [$h՛BdҞ@iءG&vVǥ8nRĩ7u\ЭD- u`ֲK³8%yhYѹJº;.!
zpg_XQKFAǿ=ȼ:ɹ8ʷ6˶5̵5͵6ζ7ϸ9к<Ѿ?DINU\dlvۀ܊ݖޢ)߯6DScs
2F[p(@Xr4Pm8Ww)Km
endstream
endobj
16 0 obj
<<
/D [13 0 R /XYZ null 259 null]
/S /GoTo
>>
endobj
17 0 obj
<<
/First 64 0 R
/Parent 2 0 R
/A 65 0 R
/Next 66 0 R
/Count -3
/Last 67 0 R
/Prev 9 0 R
/Title (Introduction to the B method)
>>
endobj
18 0 obj
<<
/D [36 0 R /XYZ null 396 null]
/S /GoTo
>>
endobj
19 0 obj
<<
/Parent 2 0 R
/A 68 0 R
/Next 10 0 R
/Prev 69 0 R
/Title (Conclusion and future work)
>>
endobj
20 0 obj
<<
/Type /Page
/Resources <<
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/ExtGState <<
/G3 70 0 R
/G11 71 0 R
/G12 72 0 R
>>
/XObject <<
/X8 73 0 R
/X10 74 0 R
/X13 75 0 R
>>
/Font <<
/F4 76 0 R
/F5 77 0 R
/F6 78 0 R
/F7 79 0 R
>>
>>
/MediaBox [0 0 594.95996 840.95996]
/Annots [80 0 R 81 0 R 82 0 R 83 0 R 84 0 R 85 0 R 86 0 R 87 0 R 88 0 R 89 0 R
90 0 R 91 0 R 92 0 R 93 0 R]
/Contents 94 0 R
/StructParents 0
/Parent 11 0 R
>>
endobj
21 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [95 0 R 96 0 R 97 0 R 98 0 R 99 0 R 100 0 R 101 0 R 102 0 R 103 0 R 104 0 R]
/Parent 11 0 R
/Contents 105 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 106 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 107 0 R
/T1_2 56 0 R
/T1_3 58 0 R
/T1_4 108 0 R
/T1_5 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
22 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [109 0 R 110 0 R 111 0 R 112 0 R 113 0 R 114 0 R 115 0 R 116 0 R]
/Parent 11 0 R
/Contents 117 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 118 0 R
/Resources <<
/Font <<
/T1_0 107 0 R
/T1_1 54 0 R
/T1_2 51 0 R
/T1_3 57 0 R
/T1_4 108 0 R
/T1_5 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
23 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [119 0 R]
/Parent 11 0 R
/Contents 120 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 121 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 56 0 R
/T1_2 57 0 R
/T1_3 55 0 R
/T1_4 108 0 R
/T1_5 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 63 0 R
>>
>>
/Type /Page
>>
endobj
24 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [122 0 R 123 0 R]
/Parent 11 0 R
/Contents 124 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 125 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 57 0 R
/T1_2 55 0 R
/T1_3 126 0 R
/T1_4 127 0 R
/T1_5 107 0 R
/T1_6 108 0 R
/T1_7 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
25 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [128 0 R 129 0 R]
/Parent 11 0 R
/Contents 130 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 131 0 R
/Resources <<
/Font <<
/T1_0 132 0 R
/T1_1 53 0 R
/T1_2 56 0 R
/T1_3 127 0 R
/T1_4 133 0 R
/T1_5 134 0 R
/T1_6 54 0 R
/T1_7 108 0 R
/T1_8 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
26 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [135 0 R 136 0 R 137 0 R 138 0 R]
/Parent 11 0 R
/Contents 139 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 140 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 51 0 R
/T1_2 57 0 R
/T1_3 108 0 R
/T1_4 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
27 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 11 0 R
/Contents 141 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 142 0 R
/Resources <<
/Font <<
/T1_0 56 0 R
/T1_1 54 0 R
/T1_2 57 0 R
/T1_3 143 0 R
/T1_4 108 0 R
/T1_5 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 63 0 R
>>
>>
/Type /Page
>>
endobj
28 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [144 0 R]
/Parent 11 0 R
/Contents 145 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 146 0 R
/Resources <<
/Font <<
/T1_10 60 0 R
/T1_0 132 0 R
/T1_1 133 0 R
/T1_2 53 0 R
/T1_3 127 0 R
/T1_4 56 0 R
/T1_5 134 0 R
/T1_6 51 0 R
/T1_7 54 0 R
/T1_8 57 0 R
/T1_9 108 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
29 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 11 0 R
/Contents 147 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 148 0 R
/Resources <<
/Font <<
/T1_10 60 0 R
/T1_0 132 0 R
/T1_1 133 0 R
/T1_2 56 0 R
/T1_3 127 0 R
/T1_4 54 0 R
/T1_5 55 0 R
/T1_6 57 0 R
/T1_7 53 0 R
/T1_8 134 0 R
/T1_9 108 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
30 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 12 0 R
/Contents 149 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 150 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 132 0 R
/T1_2 133 0 R
/T1_3 56 0 R
/T1_4 57 0 R
/T1_5 53 0 R
/T1_6 108 0 R
/T1_7 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
31 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 12 0 R
/Contents 151 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 152 0 R
/Resources <<
/Font <<
/T1_0 132 0 R
/T1_1 56 0 R
/T1_2 127 0 R
/T1_3 53 0 R
/T1_4 133 0 R
/T1_5 57 0 R
/T1_6 54 0 R
/T1_7 134 0 R
/T1_8 108 0 R
/T1_9 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
32 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 12 0 R
/Contents 153 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 154 0 R
/Resources <<
/Font <<
/T1_10 60 0 R
/T1_0 132 0 R
/T1_1 53 0 R
/T1_2 133 0 R
/T1_3 56 0 R
/T1_4 127 0 R
/T1_5 134 0 R
/T1_6 54 0 R
/T1_7 57 0 R
/T1_8 55 0 R
/T1_9 108 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
33 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [155 0 R 156 0 R]
/Parent 12 0 R
/Contents 157 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 158 0 R
/Resources <<
/Font <<
/T1_0 132 0 R
/T1_1 133 0 R
/T1_2 127 0 R
/T1_3 134 0 R
/T1_4 56 0 R
/T1_5 54 0 R
/T1_6 57 0 R
/T1_7 108 0 R
/T1_8 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
34 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [159 0 R 160 0 R 161 0 R]
/Parent 12 0 R
/Contents 162 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 163 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 56 0 R
/T1_2 57 0 R
/T1_3 108 0 R
/T1_4 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
35 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 12 0 R
/Contents 164 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 165 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 51 0 R
/T1_2 108 0 R
/T1_3 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
36 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Annots [166 0 R 167 0 R 168 0 R 169 0 R]
/Parent 12 0 R
/Contents 170 0 R
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 171 0 R
/Resources <<
/Font <<
/T1_0 54 0 R
/T1_1 51 0 R
/T1_2 56 0 R
/T1_3 53 0 R
/T1_4 59 0 R
/T1_5 132 0 R
/T1_6 108 0 R
/T1_7 60 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
>>
endobj
37 0 obj
<<
/CropBox [0.0 0.0 467.717 680.315]
/Parent 12 0 R
/Contents [172 0 R 173 0 R]
/Rotate 0
/MediaBox [0.0 0.0 467.717 680.315]
/Thumb 174 0 R
/Resources <<
/Font <<
/T1_0 56 0 R
/T1_1 53 0 R
/T1_2 132 0 R
/T1_3 108 0 R
/T1_4 60 0 R
/F6 175 0 R
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/GS0 61 0 R
/GS1 62 0 R
>>
>>
/Type /Page
/Annots [176 0 R]
>>
endobj
38 0 obj
<<
/Rect [212.704 429.095 219.477 439.147]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 177 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
39 0 obj
<<
/Rect [220.23 429.095 227.003 439.147]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 178 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
40 0 obj
<<
/Rect [382.565 288.629 392.724 295.553]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 179 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
41 0 obj
<<
/Rect [398.751 169.363 405.984 178.126]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 180 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
42 0 obj
<<
/Rect [362.691 156.035 369.924 164.797]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 181 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
43 0 obj
<<
/Rect [85.8427 129.378 93.0753 138.14]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 182 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
44 0 obj
<<
/Rect [79.4102 79.9971 159.48 92.2665]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A <<
/URI (mailto:david@dimap.ufrn.br)
/S /URI
/Type /Action
>>
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
45 0 obj
<<
/Rect [328.055 571.891 428.031 580.819]
/Subtype /Link
/BS <<
/S /S
/W 0
/Type /Border
>>
/A 183 0 R
/F 4
/Border [0 0 0]
/Type /Annot
>>
endobj
46 0 obj
<<
/Length 2624
/Filter /FlateDecode
>>
stream
HWKWL<1dʶ RCbW^tO$VCr ݂gMŷnjƦlYܼ~Dz]Xܮ7k/l}`z!pkxYSfڔ0J]pl-XV*cAJCr=m>L{O[i?TJ3?_~\يUٺg~|bhDDf0',*)%iVE2elK)H[7N͈EtR|rO?SLd\%T
[qKރSԮFX<5iz\ŷ8(;lŊJɵ%^o|U,`QZEzt(}S'(Ud 0,JP8~r%lNwqeg0r yJ>%yQ).'@ϿͧsqNvɕR{߇̠k`V,U=Xٔ6vk&+}{c#lY5V[hI ii?ϥ\s.U*
^R&LN^ZcIUaeknUHY*@ҹpwEqK
>icbEӭmB -v]mw>xѷIq6O6~HNFmȪ<7yF|OvF6jnv}hMthy&=.ܶ є?e22
wiI_@Yڪ?Rnr4jєz(L>w((bP`:A
$ZTCKĊ:`1q6p7/(ijOaٔv[£RЀWp] y8<1)ph#m4I̿Oo