革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証

Material type: 文書・図像類

Author: 山根, 智ほか

Publisher: -

Publication date: 2018-04-25

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 金沢大学理工研究域電子情報通信学系研究成果は以下の2つに大別できる．（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．...

Related materials as well as pre- and post-revision versions

https://kaken.nii.ac.jp/search/?qm=70263506

https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/

https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

Kanazawa University Repository for Academic Resources
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
Kanazawa University Repository for Academic Resources

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証
Author/Editor: 山根, 智
Yamane, Satoshi
Author Heading: 山根, 智
Yamane, Satoshi
Publication Date: 2018-04-25
Publication Date (W3CDTF): 2018-04-25
Alternative Title: Verifying safety properties of embedded assembly program using innovative software model checking
Periodical title: 平成29(2017)年度科学研究費補助金基盤研究(C) 研究成果報告書 = 2017 Fiscal Year Final Research Report
No. or year of volume/issue: 2015-04-01 - 2018-03-31
Volume: 2015-04-01 - 2018-03-31
Pages: 4p.-
Text Language Code: jpn
Subject Heading: ソフトウェアモデル検査
組込みアセンブリプログラム
抽象化精錬
ＳＭＴ
定理証明
Target Audience: 一般
Note (General): 金沢大学理工研究域電子情報通信学系
研究成果は以下の2つに大別できる．（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．このモデル検査手法はＳＭＴによる述語抽象化、ＳＭＴ有界モデル検査、ＳＭＴによる反例解析器、ＳＭＴソルバによるInterpolationを用いた精錬述語の生成からなる．なお、ＳＭＴソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた．
The research outcome can be roughly divided into the following two.(1) We have developed a minimal model constructor (constructing a minimum model with interrupt processing embedded from the assembly program) by pruning and abstraction of dynamic program analysis and execution time estimation.(2) SMT model checking method based on Abstraction and Refinement (CEGAR) was developed. This model checking method consists of predicate abstraction by SMT, SMT bounded model check, counter-example analyzer by SMT, and refinement predicate generation using Interpolation by SMT solver. As the SMT solver, Princess of Uppsala University which supports various interpolations was used.
研究課題/領域番号:15K00093, 研究期間(年度):2015-04-01 - 2018-03-31
出典：研究課題「革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証」課題番号15K00093（KAKEN：科学研究費助成事業データベース（国立情報学研究所））（https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/）を加工して作成
DOI: 10.24517/00053962
Source: https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47638&item_no=1&attribute_id=26&file_no=1
https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47638&item_no=1&attribute_id=26&file_no=1
Access Restrictions: 限定公開
Rights (production): CC BY-NC-ND
Related Material: https://kaken.nii.ac.jp/search/?qm=70263506
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/
https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 金沢大学 : 金沢大学学術情報リポジトリKURA