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.

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

项目成果

右線形右シャローな項書換え系における文脈依存停止性の決定可能性について

右线性右浅项重写系统中上下文相关停止性质的可判定性

• 发表时间: 2009
• 期刊: 信学技報SS2009-41
• 作者: 御宿義勝;酒井正彦;坂部俊樹;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

基本対称関数を付加したCNF論理式の充足可能性判定

确定添加基本对称函数的 CNF 逻辑公式的可满足性

• 发表时间: 2008
• 期刊: 電子情報通信学会ソフトウェアサイエンス研究会(SS2008-44)
• 作者: 馬野洋平;酒井正彦;西田直樹;坂部俊樹;草刈圭一朗
• 通讯作者: 草刈圭一朗

線形左シャロー項書換え系の停止性の決定可能性について

线性左浅项重写系统停止性质的可判定性

• 发表时间: 2011
• 期刊: 平成23年度電気関係学会東海支部連合大会講演論文集
• 作者: 服部達哉;酒井正彦;坂部俊樹;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

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

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

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

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

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

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