课题基金 / 基金详情

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

项目摘要

项目成果

SAKABE Toshiki的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
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年度電気関係学会東海支部連合大会講演論文集
影响因子: --
作者: [馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦]
通讯作者: 酒井正彦
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
    • 依托单位:
    海外基金