2020 Fiscal Year Research-status Report
Software Verification Based on the Theory of Transducers
| Project/Area Number |
19K11899
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | ソフトウェア検証 / トランスデューサ / オートマトン / 形式言語理論 / 文字列制約 |
|---|
| Outline of Annual Research Achievements |
本年度には，以下の研究を行なった．
＊文字列を操作するプログラムの検証の基盤となる直線形式文字列制約の充足可能性判定に関する研究を行なった．前年度までの研究で，正規トランスダクション，文字列長に関する整数制約を含む制約の充足可能性判定アルゴリズムをストリーミングトランスデューサの理論に基づき開発した．本年度には，Parikhオートマトンの考え方で，ストリーミングトランスデューサを拡張した．各遷移に整数ベクトルの重みを与え，文字列の終端でこの重みが半線形集合に所属するかで受理するかを判定できるように拡張した．この拡張により，整数引数を持つ文字列演算，文字列から整数への演算などを制約で扱えるようになった．
＊ トランスデューサの理論において重要な役割を果たす先読みに関する研究を行い，先読み付き文脈自由文法を提案した．先読み付き文脈自由文法は，文脈自由文法および解析表現文法（PEG）の拡張となっており，構文解析の統一的な理論となりうるものである．否定先読みの扱いが鍵となっており，文法を先読み付き言語の方程式と考え，空集合からの反復で意味を定義した．
＊ 前年度の研究で，先読みや後方参照を含む正規表現のマッチングの実行時間のオーダを判定する解析を開発し，解析ツールを実装した．今年度には，この解析アルゴリズムの正当性の証明を型システムの健全性の証明を参考にし，整理した．また，後方参照を含む正規表現の解析の精度を改善するため，集合と木のモナドを組み合わせたモナドを用いるアプローチについて研究を行い，解析の前半部分までの拡張を本年度に行うことができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
文字列制約の充足可能性判定手続きの応用としては，プログラムの記号実行やモデル検査で生成される制約の判定があるが，そのような制約では整数を引数する文字列演算が必要となるため，本年度の研究で行った拡張は実用性の面で重要である．また，理論的にもストリーミングトランスデューサとParikhオートマトンの組み合わせは，整数制約を含むトランスデューサの理論の枠組みとして，今後の展開が期待できる．
正規表現マッチングの計算量解析において用いた集合と木の組み合わせのモナドは理論的にはよく知られたものであるが，プログラム解析等で応用されたのは申請者が知る限り初めてであり，モナドの新たな応用として興味深いものである．
|
| Strategy for Future Research Activity |
文字列制約の充足可能性判定については，競合する充足可能性判定ソルバOstrich, Ostrich+ との比較が重要になっており，比較のための適切なベンチマーク（制約のデータセット）が必要となっている．次年度には，PyEx などの記号実行器から，正規表現マッチングなどの高度な文字列演算を含む制約の収集を行うことを検討している．
|
| Causes of Carryover |
新型コロナウイルスの感染拡大のため，多くの国内の研究集会がオンライン開催になり，また，３月に予定していた国際会議での発表が2021年9月に延期になったため，次年度使用額が生じた．次年度使用額の一部は，9月に予定されている国際会議への海外出頭のために使用する予定である．また，当面，在宅勤務が多くなるため，次年度には，在宅勤務で効率的に研究を進めるために必要な機器等の購入に使用する予定である．
|
