Study of Verification of Security of Programs based on Term Rewriting Systems and Tree Automata
Study of Verification of Security of Programs based on Term Rewriting Systems and Tree Automata
批准号:
20300010
负责人:
SAKABE Toshiki
金额:
$8.07万
依托单位:
依托单位国家:
日本
项目类别:
Grant-in-Aid for Scientific Research (B)
财政年份:
2008
资助国家:
日本
项目状态:
已结题
起止时间:
2008 至 2011
中文摘要
点击翻译按钮获取中文摘要
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
プレスブルガー文付き項書換え系における書換え帰納法について
用 Presburger 语句重写术语重写系统中的归纳法
DOI:
--
发表时间:
2008
期刊:
電子情報通信学会技術研究報告(SS2008-1)
影响因子:
--
作者:
[坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹]
通讯作者:
坂部俊樹
ビットエラー通信路におけるスケーラブルCANの動作解析
可扩展CAN在误码通信路径中的运行分析
DOI:
--
发表时间:
2008
期刊:
電子情報通信学会技術研究報告(SS2008-37) 108
影响因子:
--
作者:
[鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹]
通讯作者:
西田直樹
On Proving Termination of Constrained Term Rewriting Systemsby Elim-inating Edges from Dependency Graphs
通过消除依赖图中的边来证明约束项重写系统的终止
DOI:
--
发表时间:
2011
期刊:
LNCS
影响因子:
--
作者:
[SAKATA Tsubasa, NISHIDA Naoki, SAKABE Toshiki]
通讯作者:
SAKABE Toshiki
等式理論を法とする抽象DPLLアルゴリズムの提案
抽象DPLL算法模相等理论的提出
DOI:
--
发表时间:
2010
期刊:
平成22年度電気関係学会東海支部連合大会講演論文集
影响因子:
--
作者:
[馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦]
通讯作者:
酒井正彦
語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
关于可以将应用问题简化为基本等式集应用问题的等式集类
DOI:
--
发表时间:
2012
期刊:
電子情報通信学会ソフトウェアサイエンス研究会SS2011-47
影响因子:
--
作者:
[坂井利光, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗]
通讯作者:
草刈圭一朗
共 28 条
Type Inference of Object-Oriented Programs with Exceptions Based on Term Rewriting
-
批准号:16300005
-
项目类别:Grant-in-Aid for Scientific Research (B)
-
资助金额:$3.86万
-
财政年份:2004
-
负责人:SAKABE Toshiki
-
依托单位:
Foundamental Study on Fundational Model of Concurrent Computation
-
批准号:02680020
-
项目类别:Grant-in-Aid for General Scientific Research (C)
-
资助金额:$1.09万
-
财政年份:1990
-
负责人:SAKABE Toshiki
-
依托单位:
Abstraction of Nonterminating Processes and Its Algebraic Specification
-
批准号:63580025
-
项目类别:Grant-in-Aid for General Scientific Research (C)
-
资助金额:$1.34万
-
财政年份:1988
-
负责人:SAKABE Toshiki
-
依托单位:
海外基金