Mercurial > hg > Papers > 2016 > atton-ipsjpro

view paper/mindmap.mm @ 14:784913eb2902

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wrote section 3
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 04 Jul 2016 13:59:34 +0900
parents 84ee0b8dc02e
children
line wrap: on
line source

<map version="1.0.1">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1467104182596" ID="ID_688368422" MODIFIED="1467104546619" TEXT="Verification method of programs using Continuation based C">
<node CREATED="1467104198314" ID="ID_443591537" MODIFIED="1467104203713" POSITION="right" TEXT="CS/DS">
<node CREATED="1467104203714" ID="ID_899172723" MODIFIED="1467104212759" TEXT="CS &#x306f;&#x30b7;&#x30f3;&#x30d7;&#x30eb;&#x306a;&#x51e6;&#x7406;&#x306e;&#x307f;&#x3092;&#x542b;&#x3080;">
<node CREATED="1467104212760" ID="ID_864823502" MODIFIED="1467104216191" TEXT="&#x4e88;&#x6e2c;&#x53ef;&#x80fd;&#x6027;"/>
<node CREATED="1467104216649" ID="ID_747353230" MODIFIED="1467104226180" TEXT="&#x5358;&#x4f4d;&#x3068;&#x3057;&#x3066;&#x5c0f;&#x3055;&#x304f;"/>
<node CREATED="1467104226987" ID="ID_862092051" MODIFIED="1467104234179" TEXT="&#x7121;&#x9650;&#x30eb;&#x30fc;&#x30d7;&#x306f;&#x542b;&#x307e;&#x306a;&#x3044;"/>
<node CREATED="1467104260970" ID="ID_386883351" MODIFIED="1467104263952" TEXT="&#x691c;&#x8a3c;&#x3057;&#x3084;&#x3059;&#x3044;&#x3088;&#x3046;&#x306b;"/>
</node>
<node CREATED="1467104236048" ID="ID_266698255" MODIFIED="1467104242460" TEXT="&#x30e1;&#x30bf;&#x306a;&#x8a08;&#x7b97;">
<node CREATED="1467104242461" ID="ID_302849859" MODIFIED="1467104247752" TEXT="&#x30e1;&#x30e2;&#x30ea;&#x7ba1;&#x7406;&#x306a;&#x3069;&#x306e;&#x51e6;&#x7406;">
<node CREATED="1467104266881" ID="ID_476742009" MODIFIED="1467104272319" TEXT="linear allocator"/>
<node CREATED="1467104273276" ID="ID_203648398" MODIFIED="1467104332360" TEXT="&#x4f8b;&#x5916;&#x51e6;&#x7406;"/>
<node CREATED="1467104333074" ID="ID_1462677723" MODIFIED="1467104340241" TEXT="&#x8907;&#x96d1;&#x306a;&#x3082;&#x306e;&#x3092;&#x6392;&#x9664;"/>
</node>
<node CREATED="1467104248015" ID="ID_1557706923" MODIFIED="1467104252627" TEXT="CS&#x306e;&#x51e6;&#x7406;&#x3092;&#x4fdd;&#x5b58;&#x3059;&#x308b;&#x3088;&#x3046;&#x306b;"/>
<node CREATED="1467104252913" ID="ID_1675647762" MODIFIED="1467104904363" TEXT="&#x691c;&#x8a3c;&#x3082;&#x3053;&#x3053;&#x306b;&#x5165;&#x308b;&#x3060;&#x308d;&#x3046;"/>
<node CREATED="1467105308126" ID="ID_1673096180" MODIFIED="1467105315565" TEXT="&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x7528;&#x306e;&#x30c7;&#x30fc;&#x30bf;&#x306f;&#x30e1;&#x30bf;DS&#x306b;&#x306a;&#x308b;">
<node CREATED="1467105315566" ID="ID_1098172579" MODIFIED="1467105322338" TEXT="&#x4eca;&#x306e;&#x30b3;&#x30fc;&#x30c9;&#x3067;&#x306f; context &#x306b;&#x76f8;&#x5f53;&#x3057;&#x3066;&#x3044;&#x308b;"/>
</node>
</node>
<node CREATED="1467104301655" ID="ID_1408063984" MODIFIED="1467104307104" TEXT="&#x7d44;&#x307f;&#x5408;&#x308f;&#x305b;&#x308b;">
<node CREATED="1467104307105" ID="ID_526801636" MODIFIED="1467104314564" TEXT="meta &#x306f;&#x63a5;&#x7d9a;&#x90e8;&#x5206;&#x306b;&#x5165;&#x308b;"/>
<node CREATED="1467104317624" ID="ID_1289533340" MODIFIED="1467104325357" TEXT="&#x5207;&#x308a;&#x66ff;&#x3048;&#x3089;&#x308c;&#x308b;">
<node CREATED="1467105329015" ID="ID_1412071588" MODIFIED="1467105335666" TEXT="&#x901a;&#x5e38;&#x306e; goto &#x3059;&#x308b;&#x3060;&#x3051;&#x306e; meta"/>
<node CREATED="1467105336332" ID="ID_1717421512" MODIFIED="1467105341539" TEXT="&#x4f8b;&#x5916;&#x51e6;&#x7406;&#x4ed8;&#x304d;&#x306e; meta"/>
</node>
</node>
<node CREATED="1467104994438" ID="ID_1517687906" MODIFIED="1467105005425" TEXT="&#x4e26;&#x5217;&#x5b9f;&#x884c;">
<node CREATED="1467105005425" ID="ID_907477945" MODIFIED="1467105015773" TEXT="&#x4f9d;&#x5b58;&#x95a2;&#x4fc2;&#x304c;&#x7121;&#x3044;&#x3082;&#x306e;&#x306f;&#x81ea;&#x52d5;&#x3067;&#x5b9f;&#x884c;&#x3055;&#x308c;&#x308b;">
<node CREATED="1467105015774" ID="ID_1667782919" MODIFIED="1467105018358" TEXT="&#x3068;&#x3044;&#x3046;&#x3053;&#x3068;&#x306b;&#x306a;&#x3063;&#x3066;&#x308b;"/>
<node CREATED="1467105018583" ID="ID_1858528611" MODIFIED="1467105027965" TEXT="Gears &#x306b;&#x306f;&#x73fe;&#x5728;&#x30b9;&#x30b1;&#x30b8;&#x30e5;&#x30fc;&#x30e9;&#x304c;&#x7121;&#x3044;"/>
</node>
</node>
</node>
<node CREATED="1467104373823" ID="ID_1988531007" MODIFIED="1467104376718" POSITION="left" TEXT="CbC">
<node CREATED="1467104376719" ID="ID_1705458269" MODIFIED="1467104387375" TEXT="CS/DS &#x3092;&#x7528;&#x3044;&#x3066;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x3059;&#x308b;&#x8a00;&#x8a9e;"/>
<node CREATED="1467104389619" ID="ID_1304713196" MODIFIED="1467104406891" TEXT="CS &#x306f;&#x307b;&#x307c; C function &#x3067; goto &#x3067;&#x63a5;&#x7d9a;&#x3055;&#x308c;&#x308b;">
<node CREATED="1467105476704" ID="ID_784940950" MODIFIED="1467105494212" TEXT="for, while &#x3068;&#x3044;&#x3063;&#x305f;&#x57fa;&#x672c;&#x69cb;&#x6587;&#x306f;&#x540c;&#x3058;"/>
<node CREATED="1467105494317" ID="ID_1554202795" MODIFIED="1467105514048" TEXT="__code &#x3092; function &#x306e;&#x5b9a;&#x7fa9;&#x6642;&#x306b;&#x4ed8;&#x3051;&#x308b;&#x3068; CS &#x306b;&#x306a;&#x308b;"/>
</node>
<node CREATED="1467104415771" ID="ID_835076590" MODIFIED="1467104448948" TEXT="C &#x306e;&#x8cc7;&#x7523;&#x3092;&#x4f7f;&#x3046;&#x305f;&#x3081;&#x306b; function call &#x3082;&#x3067;&#x304d;&#x308b;">
<node CREATED="1467105516683" ID="ID_1112085216" MODIFIED="1467105523602" TEXT="printf"/>
<node CREATED="1467105523819" ID="ID_525933212" MODIFIED="1467105524983" TEXT="malloc"/>
<node CREATED="1467105525236" ID="ID_1780380433" MODIFIED="1467105531942" TEXT="pthread"/>
<node CREATED="1467105532212" ID="ID_829428193" MODIFIED="1467105536816" TEXT="&#x4ed6;&#x306e;&#x30e9;&#x30a4;&#x30d6;&#x30e9;&#x30ea;"/>
</node>
<node CREATED="1467104407232" ID="ID_1980396133" MODIFIED="1467104412679" TEXT="DS &#x306f;&#x69cb;&#x9020;&#x4f53;&#x3067;&#x8868;&#x73fe;&#x3055;&#x308c;&#x3066;&#x3044;&#x308b;">
<node CREATED="1467105537123" ID="ID_1489116959" MODIFIED="1467105552860" TEXT="&#x69cb;&#x9020;&#x4f53;&#x306e; union"/>
<node CREATED="1467105556645" ID="ID_1543655706" MODIFIED="1467105559990" TEXT="&#x81ea;&#x52d5;&#x3067;&#x751f;&#x6210;&#x3057;&#x305f;&#x3044;"/>
</node>
<node CREATED="1467104919532" ID="ID_390963158" MODIFIED="1467104927291" TEXT="implementations">
<node CREATED="1467104927292" ID="ID_1136736292" MODIFIED="1467104929949" TEXT="micro C"/>
<node CREATED="1467104930294" ID="ID_677752795" MODIFIED="1467104931309" TEXT="gcc"/>
<node CREATED="1467104931547" ID="ID_983923346" MODIFIED="1467104934833" TEXT="llvm/clang">
<node CREATED="1467104934833" ID="ID_445358833" MODIFIED="1467104941574" TEXT="&#x4eca;&#x306f;&#x3053;&#x308c;&#x3092;&#x4f7f;&#x3063;&#x3066;&#x3044;&#x308b;"/>
</node>
</node>
<node CREATED="1467105049108" ID="ID_1595654033" MODIFIED="1467105066817" TEXT="&#x4e26;&#x5217;&#x5b9f;&#x884c;">
<node CREATED="1467105066818" ID="ID_1166826550" MODIFIED="1467105081131" TEXT="&#x5404; thread &#x3067; context &#x3092;&#x6301;&#x3063;&#x3066;&#x3044;&#x3066;&#x4e26;&#x5217;&#x306b;&#x5b9f;&#x884c;&#x3067;&#x304d;&#x308b;"/>
<node CREATED="1467105081401" ID="ID_498561044" MODIFIED="1467105086823" TEXT="twice &#x304c;&#x3042;&#x308b;">
<node CREATED="1467105571389" ID="ID_265071868" MODIFIED="1467105584340" TEXT="&#x4e26;&#x5217;&#x5b9f;&#x884c;&#x306e;&#x52b9;&#x679c;&#x306f;&#x3042;&#x308b;"/>
</node>
<node CREATED="1467105087623" ID="ID_841475890" MODIFIED="1467105106414" TEXT="&#x4eca;&#x306f;&#x7d20;&#x76f4;&#x306b;meta&#x5074;&#x3067; pthread_create">
<node CREATED="1467105106415" ID="ID_1873952928" MODIFIED="1467105114189" TEXT="&#x30b9;&#x30b1;&#x30b8;&#x30e5;&#x30fc;&#x30e9;&#x3092;&#x4f5c;&#x308a;&#x305f;&#x3044;">
<node CREATED="1467105114190" ID="ID_213462348" MODIFIED="1467105125775" TEXT="Gears &#x3092; Cerium &#x3068;&#x540c;&#x3058;&#x304f;&#x3089;&#x3044;&#x306b;&#x3059;&#x308b;"/>
<node CREATED="1467105126005" ID="ID_436242008" MODIFIED="1467105133119" TEXT="&#x4f9d;&#x5b58;&#x95a2;&#x4fc2;&#x3092;&#x3069;&#x3046;&#x8a18;&#x8ff0;&#x3059;&#x308b;&#x304b;"/>
</node>
</node>
</node>
</node>
<node CREATED="1467104451097" ID="ID_1539282609" MODIFIED="1467105724456" POSITION="right" TEXT="akasha">
<node CREATED="1467104453043" ID="ID_98539964" MODIFIED="1467104458142" TEXT="&#x5b9f;&#x969b;&#x306b;&#x306f; CbC &#x306e;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;">
<node CREATED="1467105159250" ID="ID_1125168168" MODIFIED="1467105164559" TEXT="meta &#x90e8;&#x5206;&#x306e;&#x307f;&#x3092;&#x66f8;&#x3044;&#x3066;&#x3042;&#x308b;"/>
<node CREATED="1467105164862" ID="ID_1705620865" MODIFIED="1467105176202" TEXT="llrb &#x90e8;&#x5206;&#x306f;&#x5909;&#x66f4;&#x3057;&#x3066;&#x3044;&#x306a;&#x3044;">
<node CREATED="1467105176203" ID="ID_1349265303" MODIFIED="1467105183387" TEXT="&#x5b9f;&#x884c;&#x30d0;&#x30a4;&#x30ca;&#x30ea;&#x3092;&#x4f5c;&#x308b;&#x6642;&#x306b;&#x30ea;&#x30f3;&#x30af;&#x3057;&#x3066;&#x3044;&#x308b;"/>
</node>
<node CREATED="1467105187553" ID="ID_436799831" MODIFIED="1467105203039" TEXT="&#x306a;&#x306e;&#x3067; context &#x306a;&#x3069;&#x306f; akasha &#x7528;&#x306b;&#x518d;&#x4f5c;&#x6210;&#x3057;&#x3066;&#x3044;&#x308b;"/>
<node CREATED="1467105203313" ID="ID_1425319166" MODIFIED="1467105220031" TEXT="&#x30c7;&#x30fc;&#x30bf;&#x69cb;&#x9020;&#x306e;API&#x304c;&#x5909;&#x308f;&#x308b;&#x3068;&#x5909;&#x66f4;&#x305b;&#x3056;&#x308b;&#x3092;&#x5f97;&#x306a;&#x3044;">
<node CREATED="1467105220032" ID="ID_1845113140" MODIFIED="1467105225566" TEXT="&#x305d;&#x308c;&#x306f;&#x4ed6;&#x306e;&#x8a00;&#x8a9e;&#x3067;&#x3082;&#x305d;&#x3046;&#x304b;"/>
</node>
</node>
<node CREATED="1467104458392" ID="ID_691068611" MODIFIED="1467104461714" TEXT="&#x5168;&#x90e8;&#x306e;&#x72b6;&#x614b;&#x3092;&#x5217;&#x6319;&#x3059;&#x308b;">
<node CREATED="1467104488690" ID="ID_82006877" MODIFIED="1467104501575" TEXT="&#x4eca;&#x5f8c;&#x306e;&#x76ee;&#x6a19;&#x3068;&#x3057;&#x3066;&#x306f;&#x72b6;&#x614b;&#x306e;&#x62bd;&#x8c61;&#x5316;&#x3092;&#x3057;&#x3066;&#x9ad8;&#x901f;&#x5316;"/>
<node CREATED="1467104503246" ID="ID_43061191" MODIFIED="1467104506535" TEXT="&#x306a;&#x306e;&#x3067; bounded"/>
<node CREATED="1467105229544" ID="ID_1781859055" MODIFIED="1467105241412" TEXT="&#x5358;&#x306b;&#x5168;&#x63a2;&#x7d22;">
<node CREATED="1467105241413" ID="ID_1028101450" MODIFIED="1467105253896" TEXT="&#x30e1;&#x30e2;&#x30ea;&#x958b;&#x653e;&#x306e;&#x30b3;&#x30fc;&#x30c9;&#x306f;&#x5165;&#x308c;&#x3066;&#x308b;&#x306e;&#x3067;&#x30e1;&#x30e2;&#x30ea;&#x6ea2;&#x308c;&#x306f;&#x4e00;&#x5fdc;&#x3057;&#x3065;&#x3089;&#x3044;"/>
<node CREATED="1467105254159" ID="ID_956584291" MODIFIED="1467105264792" TEXT="&#x6642;&#x9593;&#x306e;&#x307f;&#x304c;&#x3072;&#x305f;&#x3059;&#x3089;&#x306b;&#x304b;&#x304b;&#x308b;"/>
</node>
<node CREATED="1467105590876" ID="ID_780135548" MODIFIED="1467105610999" TEXT="&#x5143;&#x306e;&#x30b3;&#x30fc;&#x30c9;&#x3092;&#x5909;&#x3048;&#x306a;&#x3044; + &#x5168;&#x63a2;&#x7d22;&#x306a;&#x306e;&#x3067; JavaPathFinder &#x306b;&#x8fd1;&#x3044;"/>
</node>
<node CREATED="1467104461923" ID="ID_1582798373" MODIFIED="1467104470505" TEXT="assert base &#x3067;&#x6027;&#x8cea;&#x3092;&#x66f8;&#x304f;">
<node CREATED="1467104470506" ID="ID_610847415" MODIFIED="1467105860352" TEXT="llrb &#x306e;&#x9ad8;&#x3055;&#x306e;&#x307f;&#x30c1;&#x30a7;&#x30c3;&#x30af;">
<node CREATED="1467105897059" ID="ID_1999377183" MODIFIED="1467105900533" TEXT="&#x4eca;&#x306f; insert &#x306e;&#x307f;"/>
</node>
<node CREATED="1467104478348" ID="ID_1552847590" MODIFIED="1467105272062" TEXT="counter example &#x306e;&#x51fa;&#x529b;&#x30b3;&#x30fc;&#x30c9;&#x3082;&#x81ea;&#x5206;&#x3067;&#x66f8;&#x3044;&#x3066;&#x3044;&#x308b;">
<node CREATED="1467105272590" ID="ID_414429238" MODIFIED="1467105278246" TEXT="&#x3053;&#x3053;&#x304c;&#x30d0;&#x30b0;&#x308b;&#x53ef;&#x80fd;&#x6027;&#x3082;&#x7121;&#x304f;&#x306f;&#x306a;&#x3044;"/>
<node CREATED="1467105278505" ID="ID_402375225" MODIFIED="1467105294372" TEXT="llrb &#x7528;&#x306e;&#x30b3;&#x30fc;&#x30c9;&#x306b;&#x306a;&#x3063;&#x3066;&#x308b;&#x306e;&#x3067;&#x6c4e;&#x7528;&#x6027;&#x306f;&#x7121;&#x3044;"/>
</node>
<node CREATED="1467105444061" ID="ID_668713683" MODIFIED="1467105466207" TEXT="&#x308f;&#x3056;&#x3068;&#x30d0;&#x30b0;&#x3092;llrb&#x306b;&#x4ed5;&#x8fbc;&#x3093;&#x3067;&#x3082;&#x53cd;&#x4f8b;&#x306f;&#x8fd4;&#x3057;&#x3066;&#x304f;&#x308c;&#x305f;"/>
<node CREATED="1467105903093" ID="ID_14091279" MODIFIED="1467105908213" TEXT="&#x307e;&#x3060;&#x30c1;&#x30a7;&#x30c3;&#x30af;&#x3057;&#x3066;&#x3044;&#x306a;&#x3044;&#x3053;&#x3068;">
<node CREATED="1467105848774" ID="ID_304519484" MODIFIED="1467105858494" TEXT="&#x8981;&#x7d20;&#x304c; unique &#x304b;">
<node CREATED="1467105946394" ID="ID_968623311" MODIFIED="1467105961893" TEXT="&#x5168;&#x63a2;&#x7d22;&#x3057;&#x3066;&#x3057;&#x307e;&#x3048;&#x3070;&#x554f;&#x984c;&#x7121;&#x3044;"/>
</node>
<node CREATED="1467105874927" ID="ID_271098631" MODIFIED="1467105883200" TEXT="search &#x304c;&#x304d;&#x3061;&#x3093;&#x3068;&#x3067;&#x304d;&#x308b;&#x304b;">
<node CREATED="1467105946394" ID="ID_1461377606" MODIFIED="1467105961893" TEXT="&#x5168;&#x63a2;&#x7d22;&#x3057;&#x3066;&#x3057;&#x307e;&#x3048;&#x3070;&#x554f;&#x984c;&#x7121;&#x3044;"/>
</node>
<node CREATED="1467105883552" ID="ID_521484669" MODIFIED="1467105886702" TEXT="delete &#x3067;&#x304d;&#x308b;&#x304b;">
<node CREATED="1467105937347" ID="ID_1716391119" MODIFIED="1467105944199" TEXT="delete implementation &#x304c;&#x3067;&#x304d;&#x3066;&#x304b;&#x3089;"/>
</node>
</node>
</node>
<node CREATED="1467104512049" ID="ID_1708243238" MODIFIED="1467104519894" TEXT="&#x53ef;&#x80fd;&#x306a;&#x691c;&#x8a3c;&#x8981;&#x7d20;&#x6570;">
<node CREATED="1467104519895" ID="ID_1261923924" MODIFIED="1467104524491" TEXT="&#x73fe;&#x5728;&#x306f; max 12"/>
<node CREATED="1467104524750" ID="ID_1183166569" MODIFIED="1467104836368" TEXT="1 hour &#x304f;&#x3089;&#x3044;"/>
<node CREATED="1467104836638" ID="ID_1967210895" MODIFIED="1467104842905" TEXT="&#x30e1;&#x30e2;&#x30ea;&#x306f; 1 G&#x3067;&#x8db3;&#x308a;&#x308b;"/>
</node>
<node CREATED="1467104796356" ID="ID_1248008112" MODIFIED="1467104812011" TEXT="Synchronized Queue">
<node CREATED="1467104813502" ID="ID_119764172" MODIFIED="1467104816332" TEXT="&#x307e;&#x3060;&#x30c1;&#x30a7;&#x30c3;&#x30af;&#x3057;&#x3066;&#x306a;&#x3044;"/>
<node CREATED="1467104816642" ID="ID_852145992" MODIFIED="1467104823011" TEXT="CAS &#x5468;&#x308a;&#x306e;&#x30c1;&#x30a7;&#x30c3;&#x30af;&#x3082;&#x5fc5;&#x8981;"/>
</node>
<node CREATED="1467104857827" ID="ID_807870663" MODIFIED="1467104862950" TEXT="&#x691c;&#x8a3c;&#x3067;&#x304d;&#x306a;&#x3044;&#x3053;&#x3068;">
<node CREATED="1467104862951" ID="ID_1931709274" MODIFIED="1467104872214" TEXT="CS &#x81ea;&#x4f53;&#x3067;&#x7121;&#x9650;&#x30eb;&#x30fc;&#x30d7;&#x3092;&#x5f62;&#x6210;&#x3055;&#x308c;&#x308b;"/>
<node CREATED="1467104876244" ID="ID_1257276169" MODIFIED="1467104894034" TEXT="&#x5b9f;&#x884c;&#x4e2d;&#x306b; segv &#x3059;&#x308b;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;"/>
</node>
<node CREATED="1467105360442" ID="ID_896233851" MODIFIED="1467105365288" TEXT="&#x4e26;&#x5217;&#x306b;&#x5b9f;&#x884c;&#x53ef;&#x80fd;&#x304b;">
<node CREATED="1467105365289" ID="ID_1518356839" MODIFIED="1467105381040" TEXT="&#x63a2;&#x7d22;&#x90e8;&#x5206;&#x306f;&#x4e26;&#x5217;&#x3067;&#x5b9f;&#x884c;&#x53ef;&#x80fd;&#x3060;&#x3068;&#x601d;&#x3046;">
<node CREATED="1467105381041" ID="ID_1298030876" MODIFIED="1467105418053" TEXT="&#x9ad8;&#x3005; /n &#x306a;&#x306e;&#x3067; exp &#x306b;&#x5bfe;&#x3057;&#x3066;&#x306f;&#x305d;&#x3093;&#x306a;&#x306b;&#x52b9;&#x679c;&#x7684;&#x3067;&#x306f;&#x306a;&#x3044;">
<node CREATED="1467105422353" ID="ID_268617420" MODIFIED="1467105429157" TEXT="&#x62bd;&#x8c61;&#x5316;&#x3068;&#x304b;&#x306e;&#x65b9;&#x304c;&#x52b9;&#x679c;&#x304c;&#x9ad8;&#x3044;"/>
</node>
</node>
</node>
</node>
<node CREATED="1467104547538" ID="ID_899818608" MODIFIED="1467104553523" POSITION="left" TEXT="cbmc">
<node CREATED="1467104553523" ID="ID_890713893" MODIFIED="1467104560944" TEXT="C &#x306e; bounded model checker"/>
<node CREATED="1467104561216" ID="ID_1168684794" MODIFIED="1467104568129" TEXT="&#x3053;&#x308c;&#x3082;&#x30bd;&#x30fc;&#x30b9;&#x3092;&#x5909;&#x66f4;&#x3057;&#x306a;&#x304f;&#x3066;&#x3082;&#x826f;&#x3044;">
<node CREATED="1467104772712" ID="ID_237137885" MODIFIED="1467104781153" TEXT="C &#x306e; symbolic exectution &#x3089;&#x3057;&#x3044;"/>
</node>
<node CREATED="1467104568538" ID="ID_103150222" MODIFIED="1467104580754" TEXT="&#x975e;&#x6c7a;&#x5b9a;&#x88fd;&#x3092;&#x8868;&#x73fe;&#x3067;&#x304d;&#x308b; input &#x306a;&#x3069;&#x3082; builtin &#x3067;&#x3042;&#x308b;">
<node CREATED="1467104580755" ID="ID_788717002" MODIFIED="1467104597573" TEXT="&#x305d;&#x3046;&#x3044;&#x3046;&#x610f;&#x5473;&#x3067;&#x306f;&#x691c;&#x8a3c;&#x7528;&#x30b3;&#x30fc;&#x30c9;&#x306b;&#x66f8;&#x304d;&#x63db;&#x3048;&#x306a;&#x3044;&#x3068;"/>
<node CREATED="1467104598999" ID="ID_388191542" MODIFIED="1467104651773" TEXT="cs/ds &#x3060;&#x3068;&#x5143;&#x306e;&#x51e6;&#x7406;&#x3092;&#x58ca;&#x3055;&#x306a;&#x3044;&#x4f4d;&#x7f6e;&#x306b;assert &#x3092;&#x66f8;&#x3051;&#x308b;"/>
</node>
<node CREATED="1467104654240" ID="ID_1681700868" MODIFIED="1467104669033" TEXT="cbc &#x30b3;&#x30fc;&#x30c9;&#x306f; goto &#x3092; return &#x306b;&#x3059;&#x308b;&#x3053;&#x3068;&#x3067; C &#x306b;&#x3067;&#x304d;&#x308b;"/>
<node CREATED="1467104669291" ID="ID_1379058858" MODIFIED="1467104679027" TEXT="Pointer &#x306e; null check &#x306a;&#x3069;&#x3082;&#x3067;&#x304d;&#x308b;">
<node CREATED="1467104730479" ID="ID_1451855658" MODIFIED="1467104743663" TEXT="&#x30c7;&#x30d5;&#x30a9;&#x30eb;&#x30c8;&#x3067;&#x3044;&#x304f;&#x3064;&#x304b;&#x306e;&#x691c;&#x8a3c;&#x30d7;&#x30ed;&#x30d1;&#x30c6;&#x30a3;&#x304c;&#x3042;&#x308b;"/>
<node CREATED="1467104743937" ID="ID_1832275750" MODIFIED="1467104756107" TEXT="&#x81ea;&#x524d;&#x3067;assert&#x3092;&#x66f8;&#x304f;&#x3053;&#x3068;&#x3082;&#x53ef;&#x80fd;"/>
</node>
<node CREATED="1467104679330" ID="ID_594229550" MODIFIED="1467104685379" TEXT="llrb &#x306f;&#x691c;&#x8a3c;&#x3067;&#x304d;&#x306a;&#x3044;">
<node CREATED="1467104685629" ID="ID_1180276746" MODIFIED="1467104697233" TEXT="&#x8981;&#x7d20;&#x6570;1&#x3067;&#x3082;&#x30c1;&#x30a7;&#x30c3;&#x30af;&#x4e0d;&#x53ef;">
<node CREATED="1467104697234" ID="ID_211544587" MODIFIED="1467104703238" TEXT="1000&#x884c;&#x304f;&#x3089;&#x3044;&#x306e;&#x30b3;&#x30fc;&#x30c9;"/>
<node CREATED="1467104704027" ID="ID_527386309" MODIFIED="1467104717204" TEXT="loop unwind &#x3057;&#x3059;&#x304e;&#x308b;&#x3068; memory &#x306b;&#x4e57;&#x3089;&#x306a;&#x3044;&#x3089;&#x3057;&#x3044;"/>
</node>
</node>
<node CREATED="1467104757767" ID="ID_624701293" MODIFIED="1467104767730" TEXT="counter example &#x3082;&#x51fa;&#x3057;&#x3066;&#x304f;&#x308c;&#x308b;"/>
</node>
</node>
</map>