{"updated":"2025-01-19T07:45:33.635815+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00241050","sets":["6164:6165:6617:11855"]},"path":["11855"],"owner":"44499","recid":"241050","title":["GearsOSとgearsAgda上のモデル検査について"],"pubdate":{"attribute_name":"公開日","attribute_value":"2024-11-25"},"_buckets":{"deposit":"46e2873d-7bb4-476d-ab44-90cd26de7b48"},"_deposit":{"id":"241050","pid":{"type":"depid","value":"241050","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"GearsOSとgearsAgda上のモデル検査について","author_link":["662977"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"GearsOSとgearsAgda上のモデル検査について"},{"subitem_title":"Model checking on GearsOS and gearsAgda","subitem_title_language":"en"}]},"item_type_id":"18","publish_date":"2024-11-25","item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_18_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"現在，琉球大学"}]},"item_18_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Presently with Uniersity of the Ryukyus","subitem_text_language":"en"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/241050/files/IPSJ-ComSys2024003.pdf","label":"IPSJ-ComSys2024003.pdf"},"date":[{"dateType":"Available","dateValue":"2026-11-25"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-ComSys2024003.pdf","filesize":[{"value":"1.6 MB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"11"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"d50abcd1-eb23-4067-9697-5c77fff843b7","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2024 by the Information Processing Society of Japan"}]},"item_18_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"河野, 真治"}],"nameIdentifiers":[{}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_5794","resourcetype":"conference paper"}]},"item_18_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"GearsOS は軽量継続を用いて，さまざまなプログラムを記述する．この時の記述言語として C base の CbC (Continuation based C) と，Agda baseのgearsAgda がある．CbC で記述されたプログラムは Model 検査することができるが，それには計算量がかかる．geasAgda で記述されたプログラムは，Invariant をメタレベルに導入することでさまざまな検証をおこなうことができる この論文では gearsAgda を使ったモデル検査について述べる．Buchi automaton と時相論理式の記述を Agda で記述し，それを Invariant として gearsAgda の code にいれることで検証をおこなう．gearsAgdaのfair scheduler で実行せずに，検証を行うことが可能になる したがって，正確にはモデル検査的な手法を用いたプログラムの検証になる","subitem_description_type":"Other"}]},"item_18_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"20","bibliographic_titles":[{"bibliographic_title":"コンピュータシステム・シンポジウム論文集"}],"bibliographicPageStart":"17","bibliographicIssueDates":{"bibliographicIssueDate":"2024-11-25","bibliographicIssueDateType":"Issued"},"bibliographicVolumeNumber":"2024"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"created":"2025-01-19T01:45:35.601051+00:00","id":241050,"links":{}}