文献

J-GLOBAL ID：201902240354210691   整理番号：19A1317860

分離論理によるポインタプログラム検証の完全性と表現性【JST・京大機械翻訳】

Completeness and expressiveness of pointer program verification by separation logic

著者 (3件)： Tatsuta Makoto (National Institute of Informatics, 2-1-2 Hitotsubashi, 101-8430 Tokyo, Japan) ,  Chin Wei-Ngan (Department of Computer Science, National University of Singapore, Singapore) ,  Al Ameen Mahmudul Faisal (Department of Computer Science, National University of Singapore, Singapore)
資料名： Information and Computation  (Information and Computation)
巻： 267  ページ： 1-27  発行年： 2019年 
JST資料番号： D0449A  ISSN： 0890-5401  CODEN： INFCEC  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： ポインタプログラム検証のためのReynolds分離論理システムを研究した。本論文は,あらゆる真の主張されたプログラムが論理システムにおいて証明可能であるという状態を,その完全性定理を証明した。完全性を証明するために,本論文はあらゆるプログラムの最も弱い前提条件を状態化する表現性定理を示して,あらゆる主張をいくつかの主張によって表現することができた。本論文は,帰納的定義による主張言語の拡張を導入して,健全性定理,表現性定理,および完全性定理を証明した。Copyright 2019 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 健全性 ,  *プログラム検証 ,  言語 ,  *完全性
準シソーラス用語： *表現力 ,  *ポインタ ,  *分離論理 , 【Automatic Indexing@JST】

著者キーワード (5件)： Hoareの論理 ,  分離論理 ,  完全性定理 ,  表現性定理 ,  帰納的定義

分類 (3件)： ゲーム理論  (KA03060T) ,  人工知能  (JE08000Z) ,  オートマトン理論  (JB04000O)

タイトルに関連する用語 (5件)： 分離論理 ,  ポインタ ,  プログラム検証 ,  完全性 ,  表現性