URL: https://homes.cs.aau.dk/~bt/PhDProgramAnalysis/KGLfiles/Fehnker_HRS_07.pdf
%PDF-1.2
7 0 obj
[5 0 R/XYZ null 764.9283437 null]
endobj
8 0 obj
[5 0 R/XYZ null 748.9881196 null]
endobj
9 0 obj
[5 0 R/XYZ null 748.9881196 null]
endobj
12 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F1
/FontDescriptor 11 0 R
/BaseFont/WIVETU+CMBX12
/FirstChar 33
/LastChar 196
/Widths[342.6 581 937.5 562.5 937.5 875 312.5 437.5 437.5 562.5 875 312.5 375 312.5
562.5 562.5 562.5 562.5 562.5 562.5 562.5 562.5 562.5 562.5 562.5 312.5 312.5 342.6
875 531.3 531.3 875 849.5 799.8 812.5 862.3 738.4 707.2 884.3 879.6 419 581 880.8
675.9 1067.1 879.6 844.9 768.5 844.9 839.1 625 782.4 864.6 849.5 1162 849.5 849.5
687.5 312.5 581 312.5 562.5 312.5 312.5 546.9 625 500 625 513.3 343.8 562.5 625 312.5
343.8 593.8 312.5 937.5 625 562.5 625 593.8 459.5 443.8 437.5 625 593.8 812.5 593.8
593.8 500 562.5 1125 562.5 562.5 562.5 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 675.9 937.5 875 787 750 879.6 812.5 875 812.5 875 0 0 812.5
656.3 625 625 937.5 937.5 312.5 343.8 562.5 562.5 562.5 562.5 562.5 849.5 500 574.1
812.5 875 562.5 1018.5 1143.5 875 312.5 562.5]
>>
endobj
15 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F2
/FontDescriptor 14 0 R
/BaseFont/ZXSYIQ+CMR10
/FirstChar 33
/LastChar 196
/Widths[277.8 500 833.3 500 833.3 777.8 277.8 388.9 388.9 500 777.8 277.8 333.3 277.8
500 500 500 500 500 500 500 500 500 500 500 277.8 277.8 277.8 777.8 472.2 472.2 777.8
750 708.3 722.2 763.9 680.6 652.8 784.7 750 361.1 513.9 777.8 625 916.7 750 777.8
680.6 777.8 736.1 555.6 722.2 750 750 1027.8 750 750 611.1 277.8 500 277.8 500 277.8
277.8 500 555.6 444.4 555.6 444.4 305.6 500 555.6 277.8 305.6 527.8 277.8 833.3 555.6
500 555.6 527.8 391.7 394.4 388.9 555.6 527.8 722.2 527.8 527.8 444.4 500 1000 500
500 500 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 625 833.3
777.8 694.4 666.7 750 722.2 777.8 722.2 777.8 0 0 722.2 583.3 555.6 555.6 833.3 833.3
277.8 305.6 500 500 500 500 500 750 444.4 500 722.2 777.8 500 902.8 1013.9 777.8
277.8 500]
>>
endobj
18 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F3
/FontDescriptor 17 0 R
/BaseFont/GQMYWE+CMR9
/FirstChar 33
/LastChar 196
/Widths[285.5 513.9 856.5 513.9 856.5 799.4 285.5 399.7 399.7 513.9 799.4 285.5 342.6
285.5 513.9 513.9 513.9 513.9 513.9 513.9 513.9 513.9 513.9 513.9 513.9 285.5 285.5
285.5 799.4 485.3 485.3 799.4 770.7 727.9 742.3 785 699.4 670.8 806.5 770.7 371 528.1
799.2 642.3 942 770.7 799.4 699.4 799.4 756.5 571 742.3 770.7 770.7 1056.2 770.7
770.7 628.1 285.5 513.9 285.5 513.9 285.5 285.5 513.9 571 456.8 571 457.2 314 513.9
571 285.5 314 542.4 285.5 856.5 571 513.9 571 542.4 402 405.4 399.7 571 542.4 742.3
542.4 542.4 456.8 513.9 1027.8 513.9 513.9 513.9 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 642.3 856.5 799.4 713.6 685.2 770.7 742.3 799.4
742.3 799.4 0 0 742.3 599.5 571 571 856.5 856.5 285.5 314 513.9 513.9 513.9 513.9
513.9 770.7 456.8 513.9 742.3 799.4 513.9 927.8 1042 799.4 285.5 513.9]
>>
endobj
21 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F4
/FontDescriptor 20 0 R
/BaseFont/IJGTGC+CMMI6
/FirstChar 33
/LastChar 196
/Widths[779.9 586.7 750.7 1021.9 639 487.8 811.6 1222.2 1222.2 1222.2 1222.2 379.6
379.6 638.9 638.9 638.9 638.9 638.9 638.9 638.9 638.9 638.9 638.9 638.9 638.9 379.6
379.6 963 638.9 963 638.9 658.7 924.1 926.6 883.7 998.3 899.8 775 952.9 999.5 547.7
681.6 1025.7 846.3 1161.6 967.1 934.1 780 966.5 922.1 756.7 731.1 838.1 729.6 1150.9
1001.4 726.4 837.7 509.3 509.3 509.3 1222.2 1222.2 518.5 674.9 547.7 559.1 642.5
589 600.7 607.7 725.7 445.6 511.6 660.9 401.6 1093.7 769.7 612.5 642.5 570.7 579.9
584.5 476.8 737.3 625 893.2 697.9 633.1 596.1 445.6 479.2 787.2 638.9 379.6 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 742.6 1027.8 934.1 859.3
907.4 999.5 951.6 736.1 833.3 781.2 0 0 946 804.5 698 652 566.2 523.3 571.8 644 590.3
466.4 725.7 736.1 750 621.5 571.8 726.7 639 716.5 582.1 689.8 742.1 767.4 819.4 379.6]
>>
endobj
24 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F5
/FontDescriptor 23 0 R
/BaseFont/FIWDYT+CMBX9
/FirstChar 33
/LastChar 196
/Widths[360.2 617.6 986.1 591.7 986.1 920.4 328.7 460.2 460.2 591.7 920.4 328.7 394.4
328.7 591.7 591.7 591.7 591.7 591.7 591.7 591.7 591.7 591.7 591.7 591.7 328.7 328.7
360.2 920.4 558.8 558.8 920.4 892.9 840.9 854.6 906.6 776.5 743.7 929.9 924.4 446.3
610.8 925.8 710.8 1121.6 924.4 888.9 808 888.9 886.7 657.4 823.1 908.6 892.9 1221.6
892.9 892.9 723.1 328.7 617.6 328.7 591.7 328.7 328.7 575.2 657.4 525.9 657.4 543
361.6 591.7 657.4 328.7 361.6 624.5 328.7 986.1 657.4 591.7 657.4 624.5 488.1 466.8
460.2 657.4 624.5 854.6 624.5 624.5 525.9 591.7 1183.3 591.7 591.7 591.7 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 710.8 986.1 920.4 827.2
788.9 924.4 854.6 920.4 854.6 920.4 0 0 854.6 690.3 657.4 657.4 986.1 986.1 328.7
361.6 591.7 591.7 591.7 591.7 591.7 892.9 525.9 616.8 854.6 920.4 591.7 1071 1202.5
920.4 328.7 591.7]
>>
endobj
27 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F6
/FontDescriptor 26 0 R
/BaseFont/NLKYFL+CMTI9
/FirstChar 33
/LastChar 196
/Widths[314.8 527.8 839.5 786.1 839.5 787 314.8 419.8 419.8 524.7 787 314.8 367.3
314.8 524.7 524.7 524.7 524.7 524.7 524.7 524.7 524.7 524.7 524.7 524.7 314.8 314.8
314.8 787 524.7 524.7 787 763 722.5 734.6 775 696.3 670.1 794.1 763 395.7 538.9 789.2
643.8 920.4 763 787 696.3 787 748.8 577.2 734.6 763 763 1025.3 763 763 629.6 314.8
527.8 314.8 524.7 314.8 314.8 524.7 472.2 472.2 524.7 472.2 314.8 472.2 524.7 314.8
314.8 472.2 262.3 839.5 577.2 524.7 524.7 472.2 432.9 419.8 341.1 550.9 472.2 682.1
473.8 498.5 419.8 524.7 1049.4 524.7 524.7 524.7 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 643.8 839.5 787 710.5 682.1 763 734.6 787 734.6
787 0 0 734.6 629.6 577.2 603.4 905.1 918.2 314.8 341.1 524.7 524.7 524.7 524.7 524.7
850.9 472.2 550.9 734.6 734.6 524.7 906.2 1011.1 787 262.3 524.7]
>>
endobj
28 0 obj
[5 0 R/XYZ null 458.6769603 null]
endobj
29 0 obj
<<
/Rect[157.46 348.74 164.44 357.16]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.Tuch_KH_05)
>>
endobj
30 0 obj
<<
/Rect[165.21 348.74 172.19 357.16]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.hohmuth_05)
>>
endobj
31 0 obj
<<
/Rect[172.96 348.74 179.94 357.16]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.Verisoft05)
>>
endobj
33 0 obj
<<
/Filter[/FlateDecode]
/Length 2436
>>
stream
xڍ˒�6�_�#T�h������z+5��hˇ8I\��Ǫ�����4R��BݍF��Oz������~��c腉'�v���&M���?��:ݜ]�V�8Oԇv��2���!8U�g7�V��~@��U*m�����,��ۄ�_����?��^�`u5����>F^�
�Is�A�RrmaW���"R��}[E�2v��H���=���q�VQ�� ����D�����nǓg��if��)I��+&���O
��I�'=�=(�%�����I�F�XSk��2�|F|UOHT�ݿ��}�~Y � �b���?���q J��,8��OW���a����~��y�ӟ�q8��ʠ���R�0��2ő����
(�U�\��^x�a���]g�ا�/�l�/
�;��J��n�D~�62����@�z�l���ʽ�Q�W�����l�zO�z|���O<��z�� �v���ƚ�͙aGmw>��d %������$`U}�� �?M���Mul��G��l��iLw ?C`��è���;��X
�Fx��3�\��ɚ�v�7-�3��Kԕc�0�BP
� N���ѡ�1��<�i_�����U�+}��d�#3
f憹u|d��+AYgp'8.J
���ĥH�d��DE�#m"����Ӯ�6OϟyU�� �T<0�Es�N�����n}�:|�崸��`Ի�5Α��rW���.�B���E�_��ul]@9�C�b�*R��;�P�7�h����!���^8�7wf�9>�j�Ñ���f��뛑�ɇ��;3��v���e<8�ײ�]��g�
�ͯ#F�(S�t��f�gȉ�a����
��ϙ�T(�7NI���G#���-pߙ�[�w�Q"
B�S���:�9�g�/Ǻ1Lq�@��~`���3D������US��#z�����\��Q3��+JL�l9��<�S6�~i���fY"a�U�Dt6R�~������X6m���Ŋz��U$�.��R/oE��<�4
\K��IO��k����,I����EE�A��9
�IX�~$v�bz%�$��_�j�u���i1Ŵ�$� /�zd�<�P��7�z����0�ڲ9���g��>��4����m�s?+��^E�b���ְH'2v-
zb(l��|�r�=���)�AI\'�W�`��۩���{/������O"��6a%��d,�ڍ�!okA�`u`B;��=#Łh2
����lq�(�]�m4��8�.���˝ w}���r�+�|�R�(���d����X�0���/�W0ٔ��
�y�њ?GH3�w
�%��b�
�B��v\9|%�G&��<8������ 5E�L�Χ����ٹ�H�c$iƝ�B��R��.I���� ����e��L�(ɔ����[:=6���s��c{� �R7N�X�\2EN3�)9����d @@�����FK�a��a�&��Asn�mWY|}�3xQ��G��O�nr��[��2���%6���
]bK?��vo�ؔ]��+t���ލ'Ґ�,��`N���%�)̵%"�4�ly��2�:���`�]�O#{zQJ�� *�4�-.��3*=�#no�&7ǩ�J<R]E
P���K��`u�f eg�.�+7��k�����؆8���cly=�eqL��ء�N��㑼ɐ��*LЙ�(�w����G�ɷ��=�NFz`ɿ=d?�a�`�!�g���kR��������ڝ�5�)�"���"��f��;PN�a�s�DGO
�Vۍ��"�S�30�(E00��^�����D��?�s0�FSA
x)��䱾����=��6�Z3�V��~���p��.y��N��z��z+\QoE�oZI��S�˥#� ��^.�Fnr�d���!��D7�; �Q��+���#��a
��|�>����ӳ_"�^��S��9�.���������)"�vq�s���Et�G���#p ����T^�{�[tU`K��ؠ�P.������υ�K9�8^�_�X��{'���t�+��9h6u[�+.�89Q��o�~[�H�H2�1�[�^G�,�B�e��*�0J1����ɖD���@�Ⱦ+�d�(��y���oh�c�uw+��v����K!���:կiR�I�Pؖ���x�T�.��ԏ��~P�_��߈I�oD�\�F�%9WJ.�BE���dH$��uL�i�.�t��1p��gs�vh���l��yy��N������?+����B~'�ڮ�Dqt���?���D��]&��<�p�����
�m% �4{�=�5%G�*Gۏ�=�\��O�p�-�����_����`�?var%��(1��S�J��ԇ�i���+�?J�{f{���I�U
endstream
endobj
35 0 obj
[29 0 R 30 0 R 31 0 R]
endobj
36 0 obj
<<
/F1 12 0 R
/F2 15 0 R
/F3 18 0 R
/F4 21 0 R
/F5 24 0 R
/F6 27 0 R
>>
endobj
6 0 obj
<<
/ProcSet[/PDF/Text/ImageC]
/Font 36 0 R
>>
endobj
39 0 obj
[37 0 R/XYZ null 764.9283437 null]
endobj
40 0 obj
<<
/Rect[136.53 690.12 143.51 698.54]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.blast)
>>
endobj
41 0 obj
<<
/Rect[144.28 690.12 151.26 698.54]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.slam)
>>
endobj
42 0 obj
<<
/Rect[152.03 690.12 159.01 698.54]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.cmbc)
>>
endobj
43 0 obj
<<
/Rect[159.78 690.12 166.76 698.54]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.magic)
>>
endobj
44 0 obj
<<
/Rect[161.1 678.16 168.08 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.sk05)
>>
endobj
45 0 obj
<<
/Rect[168.85 678.16 175.83 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.ml06)
>>
endobj
46 0 obj
<<
/Rect[428.67 678.16 440.63 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.coverity)
>>
endobj
47 0 obj
<<
/Rect[441.4 678.16 453.36 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.flexelint)
>>
endobj
48 0 obj
<<
/Rect[454.13 678.16 466.09 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.klocwork)
>>
endobj
49 0 obj
<<
/Rect[466.86 678.16 478.82 686.58]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.prefast)
>>
endobj
50 0 obj
<<
/Rect[401.76 546.44 413.72 554.87]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.nusmv2)
>>
endobj
53 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F7
/FontDescriptor 52 0 R
/BaseFont/AWHPKG+CMTI10
/FirstChar 33
/LastChar 196
/Widths[306.7 514.4 817.8 769.1 817.8 766.7 306.7 408.9 408.9 511.1 766.7 306.7 357.8
306.7 511.1 511.1 511.1 511.1 511.1 511.1 511.1 511.1 511.1 511.1 511.1 306.7 306.7
306.7 766.7 511.1 511.1 766.7 743.3 703.9 715.6 755 678.3 652.8 773.6 743.3 385.6
525 768.9 627.2 896.7 743.3 766.7 678.3 766.7 729.4 562.2 715.6 743.3 743.3 998.9
743.3 743.3 613.3 306.7 514.4 306.7 511.1 306.7 306.7 511.1 460 460 511.1 460 306.7
460 511.1 306.7 306.7 460 255.6 817.8 562.2 511.1 511.1 460 421.7 408.9 332.2 536.7
460 664.4 463.9 485.6 408.9 511.1 1022.2 511.1 511.1 511.1 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 627.2 817.8 766.7 692.2 664.4 743.3 715.6
766.7 715.6 766.7 0 0 715.6 613.3 562.2 587.8 881.7 894.4 306.7 332.2 511.1 511.1
511.1 511.1 511.1 831.3 460 536.7 715.6 715.6 511.1 882.8 985 766.7 255.6 511.1]
>>
endobj
54 0 obj
<<
/Rect[183.25 498.42 190.23 506.84]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(section.1.2)
>>
endobj
55 0 obj
<<
/Rect[411.7 498.42 418.69 506.84]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(section.1.3)
>>
endobj
56 0 obj
<<
/Rect[308.96 486.46 315.95 494.88]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(section.1.4)
>>
endobj
57 0 obj
[37 0 R/XYZ null 478.8015663 null]
endobj
58 0 obj
<<
/Rect[454.13 404.67 466.09 413.1]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.ss98)
>>
endobj
59 0 obj
<<
/Rect[466.86 404.67 478.82 413.1]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.schmidt98)
>>
endobj
60 0 obj
<<
/Rect[238.21 392.72 250.17 401.14]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.holzmann02static)
>>
endobj
61 0 obj
<<
/Rect[250.94 392.72 262.9 401.14]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.DN04)
>>
endobj
62 0 obj
<<
/Rect[445.76 332.74 457.72 341.16]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(cite.fhjlr07)
>>
endobj
65 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F8
/FontDescriptor 64 0 R
/BaseFont/WVSWMS+CMMI10
/FirstChar 33
/LastChar 196
/Widths[622.5 466.3 591.4 828.1 517 362.8 654.2 1000 1000 1000 1000 277.8 277.8 500
500 500 500 500 500 500 500 500 500 500 500 277.8 277.8 777.8 500 777.8 500 530.9
750 758.5 714.7 827.9 738.2 643.1 786.2 831.3 439.6 554.5 849.3 680.6 970.1 803.5
762.8 642 790.6 759.3 613.2 584.4 682.8 583.3 944.4 828.5 580.6 682.6 388.9 388.9
388.9 1000 1000 416.7 528.6 429.2 432.8 520.5 465.6 489.6 477 576.2 344.5 411.8 520.6
298.4 878 600.2 484.7 503.1 446.4 451.2 468.8 361.1 572.5 484.7 715.9 571.5 490.3
465 322.5 384 636.5 500 277.8 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 615.3 833.3 762.8 694.4 742.4 831.3 779.9 583.3 666.7 612.2 0 0 772.4
639.7 565.6 517.7 444.4 405.9 437.5 496.5 469.4 353.9 576.2 583.3 602.5 494 437.5
570 517 571.4 437.2 540.3 595.8 625.7 651.4 277.8]
>>
endobj
68 0 obj
<<
/Type/Font
/Subtype/Type1
/Name/F9
/FontDescriptor 67 0 R
/BaseFont/ZPLBAG+CMMI7
/FirstChar 33
/LastChar 196
/Widths[719.7 539.7 689.9 950 592.7 439.2 751.4 1138.9 1138.9 1138.9 1138.9 339.3
339.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 585.3 339.3
339.3 892.9 585.3 892.9 585.3 610.1 859.1 863.2 819.4 934.1 838.7 724.5 889.4 935.6
506.3 632 959.9 783.7 1089.4 904.9 868.9 727.3 899.7 860.6 701.5 674.8 778.2 674.6
1074.4 936.9 671.5 778.4 462.3 462.3 462.3 1138.9 1138.9 478.2 619.7 502.4 510.5
594.7 542 557.1 557.3 668.8 404.2 472.7 607.3 361.3 1013.7 706.2 563.9 588.9 523.6
530.4 539.2 431.6 675.4 571.4 826.4 647.8 579.4 545.8 398.6 442 730.1 585.3 339.3
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 693.8 954.4 868.9
797.6 844.5 935.6 886.3 677.6 769.8 716.9 0 0 880 742.7 647.8 600.1 519.2 476.1 519.8
588.6 544.1 422.8 668.8 677.6 694.6 572.8 519.8 668 592.7 662 526.8 632.9 686.9 713.8
756 339.3]
>>
endobj
69 0 obj
<<
/Rect[449.01 188.86 456 197.28]
/Type/Annot
/Subtype/Link
/C[0 1 1]
/Dest(figure.1.1)
>>
endobj
70 0 obj
<<
/Filter[/FlateDecode]
/Length 3213
>>
stream
xڍZK�۸��W�H�J4I�'�uR�[��dk0$$�L�
)z����(i�rtl����UF�j�����_��=���|��[�IXd�m�C�W��3H�[I�>�F�Ok���}[':�ÆG���T��"�F�q�D�*����f����������z���U)��iX� N�$����� L<���Am�-��`i�oM�g��?�0u�)>�*8�Z��}�|I��2�:Ƀ3ǁ����D��ȌM���V��`ۚaD�W[�9��2#�� k�H(�w>8�i���T�����O?aS����82�L��EPO��!�,$�t��_�Ž����D'F2�����Z$�$!�Z�B�K�'
��e�ga���s֎�#Q��>q�U��>1�:Lҷf�8���}"(ƛ�Ԛt�J,