Study of Verification of Security of Programs based on Term Rewriting Systems and Tree Automata

基于术语重写系统和树自动机的程序安全性验证研究

• 批准号: 20300010
• 负责人: SAKABE Toshiki
• 金额: $ 8.07万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20300010/
• 关键词: 仕様記述; 仕様検証; 安全性; 非干渉性; 項書き換え系; 木オートマトン; SMTソルバー; ホオートマトン; モデル検査; 車載LANプロトコル

The purpose of this project is to develop methods for verifying properties of programs by applying techniques of term rewriting and tree automata. The results are methods for verifying automotive LAN protocols and proving program equivalence, and automated generation of loop invariants of imperative programs. In addition, we have obtained several results which are basic to program verification : methods for proving termination of term rewriting systems, efficient SAT solvers for propositional logic and SMT solvers for equational logic.

这个项目的目的是通过应用项重写和树自动机技术来开发验证程序属性的方法。其结果是验证汽车局域网协议和证明程序等价性，并自动生成循环不变的命令式程序的方法。此外，我们还得到了几个结果，这是基本的程序验证：方法证明终止的长期重写系统，有效的SAT求解器命题逻辑和SMT求解器方程逻辑。

项目成果

プレスブルガー文付き項書換え系における書換え帰納法について

用 Presburger 语句重写术语重写系统中的归纳法

• 发表时间: 2008
• 期刊: 電子情報通信学会技術研究報告(SS2008-1)
• 作者: 坂田翼;西田直樹;酒井正彦;草刈圭一朗;坂部俊樹
• 通讯作者: 坂部俊樹

ビットエラー通信路におけるスケーラブルCANの動作解析

可扩展CAN在误码通信路径中的运行分析

• 发表时间: 2008
• 期刊: 電子情報通信学会技術研究報告(SS2008-37) 108
• 作者: 鵜飼謙児;坂部俊樹;高田広章;倉地亮;酒井正彦;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

On Proving Termination of Constrained Term Rewriting Systemsby Elim-inating Edges from Dependency Graphs

通过消除依赖图中的边来证明约束项重写系统的终止

• 发表时间: 2011
• 期刊: LNCS
• 作者: SAKATA Tsubasa;NISHIDA Naoki;SAKABE Toshiki
• 通讯作者: SAKABE Toshiki

スケーラブルCANプロトコルの動作解析に関する予備的考察

可扩展CAN协议运行分析的初步思考

• 发表时间: 2008
• 期刊: 平成20年度電気関係学会東海支部連合大会講演論文集 O-262
• 作者: 鵜飼謙児;坂部俊樹;高田広章;倉地亮;酒井正彦;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

制約付き木オートマトンとその閉包性

约束树自动机及其闭包性质

• 发表时间: 2011
• 期刊: 電子情報通信学会ソフトウェアサイエンス研究会
• 作者: 倉橋克尚;酒井正彦;西田直樹;坂部俊樹;草刈圭一朗
• 通讯作者: 草刈圭一朗