ログイン
言語:

WEKO3

  • トップ
  • コミュニティ
  • ランキング
AND
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_buckets": {"deposit": "09cc6d4b-437c-4888-88a7-23735a06f124"}, "_deposit": {"id": "21410", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "21410"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00021410"}, "item_10_alternative_title_19": {"attribute_name": "\u305d\u306e\u4ed6\u306e\u8a00\u8a9e\u306e\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_alternative_title": "Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls"}]}, "item_10_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2012-01", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "405", "bibliographicPageEnd": "44", "bibliographicPageStart": "39", "bibliographicVolumeNumber": "111", "bibliographic_titles": [{"bibliographic_title": "\u96fb\u5b50\u60c5\u5831\u901a\u4fe1\u5b66\u4f1a\u6280\u8853\u7814\u7a76\u5831\u544a. MSS, \u30b7\u30b9\u30c6\u30e0\u6570\u7406\u3068\u5fdc\u7528"}]}]}, "item_10_description_4": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "\u30d7\u30ed\u30b0\u30e9\u30e0\u691c\u8a3c\u306b\u304a\u3044\u3066,\u30eb\u30fc\u30d7\u5b9f\u884c\u4e2d\u306b\u5e38\u306b\u6210\u308a\u7acb\u3064\u8ad6\u7406\u5f0f\u3067\u3042\u308b\u4e0d\u5909\u5f0f\u304c\u91cd\u8981\u306a\u5f79\u5272\u3092\u6301\u3063\u3066\u3044\u308b.\u3057\u304b\u3057,\u691c\u8a3c\u306b\u6709\u52b9\u306a\u30eb\u30fc\u30d7\u4e0d\u5909\u5f0f\u3092\u81ea\u52d5\u7684\u306b\u767a\u898b\u3059\u308b\u3053\u3068\u306f\u4e00\u822c\u306b\u306f\u56f0\u96e3\u3067\u3042\u308b.\u672c\u7a3f\u3067\u306f,\u30d7\u30ed\u30b0\u30e9\u30e0\u5909\u6570\u3068\u95a2\u6570\u547c\u3073\u51fa\u3057\u9805\u306b\u95a2\u3059\u308b\u975e\u7dda\u5f62\u306e\u4e0d\u7b49\u5f0f\u3067\u8868\u3055\u308c\u308b\u30eb\u30fc\u30d7\u4e0d\u5909\u5f0f\u3092,\u7dda\u5f62\u8a08\u753b\u6cd5\u306a\u3069\u3067\u5229\u7528\u3055\u308c\u308bFarkas\u306e\u88dc\u984c\u3092\u62e1\u5f35\u3057\u305f\u5b9a\u7406\u306b\u57fa\u3065\u3044\u3066\u81ea\u52d5\u751f\u6210\u3059\u308b\u624b\u6cd5\u3092\u793a\u3059. Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be included, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas\u0027 Lemma.", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "URI", "subitem_identifier_uri": "http://ci.nii.ac.jp/naid/110009480932/"}, {"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/23554"}]}, "item_10_publisher_32": {"attribute_name": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "\u4e00\u822c\u793e\u56e3\u6cd5\u4eba\u96fb\u5b50\u60c5\u5831\u901a\u4fe1\u5b66\u4f1a"}]}, "item_10_relation_40": {"attribute_name": "\u30b7\u30ea\u30fc\u30ba", "attribute_value_mlt": [{"subitem_relation_name": [{"subitem_relation_name_text": "IEICE Technical Report;MSS2011-61"}]}, {"subitem_relation_name": [{"subitem_relation_name_text": "IEICE Technical Report;SS2011-46"}]}]}, "item_10_rights_12": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "(c)\u4e00\u822c\u793e\u56e3\u6cd5\u4eba\u96fb\u5b50\u60c5\u5831\u901a\u4fe1\u5b66\u4f1a \u672c\u6587\u30c7\u30fc\u30bf\u306f\u5b66\u5354\u4f1a\u306e\u8a31\u8afe\u306b\u57fa\u3065\u304dCiNii\u304b\u3089\u8907\u88fd\u3057\u305f\u3082\u306e\u3067\u3042\u308b"}]}, "item_10_select_15": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0913-5685", "subitem_source_identifier_type": "ISSN"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "\u9234\u6728, \u82f1\u4e00"}], "nameIdentifiers": [{"nameIdentifier": "62085", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u5742\u90e8, \u4fca\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "62086", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u9152\u4e95, \u6b63\u5f66"}], "nameIdentifiers": [{"nameIdentifier": "62087", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u8349\u5208, \u572d\u4e00\u6717"}], "nameIdentifiers": [{"nameIdentifier": "62088", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u897f\u7530, \u76f4\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "62089", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SUZUKI, Eiichi"}], "nameIdentifiers": [{"nameIdentifier": "62090", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki"}], "nameIdentifiers": [{"nameIdentifier": "62091", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko"}], "nameIdentifiers": [{"nameIdentifier": "62092", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "KUSAKARI, Keiichirou"}], "nameIdentifiers": [{"nameIdentifier": "62093", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "NISHIDA, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "62094", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-01"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "110009480932.pdf", "filesize": [{"value": "751.2 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 751200.0, "url": {"label": "110009480932.pdf", "url": "https://nagoya.repo.nii.ac.jp/record/21410/files/110009480932.pdf"}, "version_id": "5093b91b-e847-401f-a50b-cc28c62aa5a2"}]}, "item_keyword": {"attribute_name": "\u30ad\u30fc\u30ef\u30fc\u30c9", "attribute_value_mlt": [{"subitem_subject": "\u9759\u7684\u89e3\u6790", "subitem_subject_scheme": "Other"}, {"subitem_subject": "\u30d7\u30ed\u30b0\u30e9\u30e0\u691c\u8a3c", "subitem_subject_scheme": "Other"}, {"subitem_subject": "\u4e0d\u5909\u5f0f\u751f\u6210", "subitem_subject_scheme": "Other"}, {"subitem_subject": "\u6700\u5f31\u4e8b\u524d\u6761\u4ef6", "subitem_subject_scheme": "Other"}, {"subitem_subject": "static analysis", "subitem_subject_scheme": "Other"}, {"subitem_subject": "program verification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "invariant generation", "subitem_subject_scheme": "Other"}, {"subitem_subject": "weakest preconditon", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "\u95a2\u6570\u547c\u3073\u51fa\u3057\u3092\u6301\u3064\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u975e\u7dda\u5f62\u30eb\u30fc\u30d7\u4e0d\u5909\u5f0f\u306e\u81ea\u52d5\u751f\u6210", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "\u95a2\u6570\u547c\u3073\u51fa\u3057\u3092\u6301\u3064\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u975e\u7dda\u5f62\u30eb\u30fc\u30d7\u4e0d\u5909\u5f0f\u306e\u81ea\u52d5\u751f\u6210"}]}, "item_type_id": "10", "owner": "1", "path": ["312/313/314"], "permalink_uri": "http://hdl.handle.net/2237/23554", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_value": "2016-02-23"}, "publish_date": "2016-02-23", "publish_status": "0", "recid": "21410", "relation": {}, "relation_version_is_last": true, "title": ["\u95a2\u6570\u547c\u3073\u51fa\u3057\u3092\u6301\u3064\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u975e\u7dda\u5f62\u30eb\u30fc\u30d7\u4e0d\u5909\u5f0f\u306e\u81ea\u52d5\u751f\u6210"], "weko_shared_id": null}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

関数呼び出しを持つプログラムの非線形ループ不変式の自動生成

http://hdl.handle.net/2237/23554
62255180-08ff-4c87-b24a-d25e18ae722f
名前 / ファイル ライセンス アクション
110009480932.pdf 110009480932.pdf (751.2 kB)
Item type 学術雑誌論文 / Journal Article(1)
公開日 2016-02-23
タイトル
タイトル 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
その他のタイトル
その他のタイトル Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls
著者 鈴木, 英一

× 鈴木, 英一

WEKO 62085

鈴木, 英一

Search repository
坂部, 俊樹

× 坂部, 俊樹

WEKO 62086

坂部, 俊樹

Search repository
酒井, 正彦

× 酒井, 正彦

WEKO 62087

酒井, 正彦

Search repository
草刈, 圭一朗

× 草刈, 圭一朗

WEKO 62088

草刈, 圭一朗

Search repository
西田, 直樹

× 西田, 直樹

WEKO 62089

西田, 直樹

Search repository
SUZUKI, Eiichi

× SUZUKI, Eiichi

WEKO 62090

SUZUKI, Eiichi

Search repository
SAKABE, Toshiki

× SAKABE, Toshiki

WEKO 62091

SAKABE, Toshiki

Search repository
SAKAI, Masahiko

× SAKAI, Masahiko

WEKO 62092

SAKAI, Masahiko

Search repository
KUSAKARI, Keiichirou

× KUSAKARI, Keiichirou

WEKO 62093

KUSAKARI, Keiichirou

Search repository
NISHIDA, Naoki

× NISHIDA, Naoki

WEKO 62094

NISHIDA, Naoki

Search repository
権利
権利情報 (c)一般社団法人電子情報通信学会 本文データは学協会の許諾に基づきCiNiiから複製したものである
キーワード
主題Scheme Other
主題 静的解析
キーワード
主題Scheme Other
主題 プログラム検証
キーワード
主題Scheme Other
主題 不変式生成
キーワード
主題Scheme Other
主題 最弱事前条件
キーワード
主題Scheme Other
主題 static analysis
キーワード
主題Scheme Other
主題 program verification
キーワード
主題Scheme Other
主題 invariant generation
キーワード
主題Scheme Other
主題 weakest preconditon
抄録
内容記述 プログラム検証において,ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている.しかし,検証に有効なループ不変式を自動的に発見することは一般には困難である.本稿では,プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を,線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す. Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be included, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas' Lemma.
内容記述タイプ Abstract
出版者
出版者 一般社団法人電子情報通信学会
言語
言語 jpn
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
ISSN
収録物識別子タイプ ISSN
収録物識別子 0913-5685
書誌情報 電子情報通信学会技術研究報告. MSS, システム数理と応用

巻 111, 号 405, p. 39-44, 発行日 2012-01
著者版フラグ
値 publisher
シリーズ
関連名称
関連名称 IEICE Technical Report;MSS2011-61
シリーズ
関連名称
関連名称 IEICE Technical Report;SS2011-46
URI
識別子 http://ci.nii.ac.jp/naid/110009480932/
識別子タイプ URI
URI
識別子 http://hdl.handle.net/2237/23554
識別子タイプ HDL
戻る
0
views
See details
Views

Versions

Ver.1 2021-03-01 15:23:39.324017
Show All versions

Share

Mendeley CiteULike Twitter Facebook Print Addthis

Cite as

Export

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by CERN Data Centre & Invenio


Powered by CERN Data Centre & Invenio