2015 Fiscal Year Annual Research Report
新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用
| Project/Area Number |
24680001
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 准教授 (60456762)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / システム検証 / 形式検証 / 物理情報システム / ハイブリッドシステム / 関数型プログラミング / 量子計算 / 不動点論理 |
|---|
| Outline of Annual Research Achievements |
獲得目標１（ハイブリッドシステムの自動検証）については，超準アプローチにおけるスケーラビリティの課題を Cousot-Cousot の抽象解釈によって乗り越える試みについての論文が，抽象解釈とシステム検証に関する国際会議 VMCAI 2016 に採択された．また別に，産業界のモデルベース開発の現場における反例生成の重要性に鑑み，仕様記述言語（時相論理）に《平均化様相演算子》を導入して，確率的最適化による反例生成を効率化する研究について，論文がシステム検証分野のトップ国際会議 CAV 2015 に採択された．後者は特に優れた論文として，学術誌特集号への招待を受けた（現在査読中）．
獲得目標２（量子計算のための抽象機械）については，量子計算など（関数型計算における）一般の計算副作用について，GoI 式の抽象機械を一挙に与える圏論的枠組みについて研究を継続した．前年度得られた枠組み [Hoshino, Muroya & Hasuo, CSL-LICS 2014] に《再帰》を導入し，上記 GoI 抽象機械と（自然な，Plotkin & Power 式の）操作的意味論との間の関係性（妥当性 adequacy）を示した成果は，プログラミング言語分野のトップ国際会議 POPL 2016 に採択された．
さらに，上記獲得目標を含む具体的応用に通底する理論的基盤として，仕様記述のための不動点論理，特に最小不動点（活性）と最大不動点（安全性）が交替で現れる仕様の数学的基礎の研究に取り組んだ．この成果はプログラミング言語分野のトップ国際会議 POPL 2016 に採択された．このような交替性不動点論理式は，（様相μ計算で仕様が記述される）古典的なモデル検査においてはもちろん，近年では制御理論における recurrence や persistence など，より広いヘテロジニアス・システムの品質保証の文脈で重要視されており，今後上記成果の幅広い応用について研究を進めていく計画である．
|
| Research Progress Status |
27年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
27年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
27年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
27年度が最終年度であるため、記入しない。
|
Research Products
(26 results)
-
-
-
-
-
-
-
[Journal Article] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
-
Journal Title
Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Volume: なし
Pages: 未定
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
[Presentation] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
Organizer
Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Place of Presentation
New York City, USA
Year and Date
2016-07-05 – 2016-07-08
Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
