文献

J-GLOBAL ID：201702222206013555   整理番号：17A1286464

Z3に基づくCoq自動証明戦略の設計と実現【JST・京大機械翻訳】

Design and Implementation of Coq Tactics Based on Z3

著者 (2件)： Zhang Hengruo (中国科学技術大学信息科学技術学院,安徽合肥,230026) ,  Fu Ming (中国科学技術大学計算机科学与技術学院,安徽合肥230026;中国科学技術大学蘇州研究院軟件安全実験室,江蘇蘇州215123)
資料名： Ruanjian Xuebao  (Ruanjian Xuebao)
巻： 28  号： 4  ページ： 819-826  発行年： 2017年 
JST資料番号： C2542A  ISSN： 1000-9825  CODEN： RUXUEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： 形式的検証法は高信頼ソフトウェアシステムを構築する有効な手段であると考えられている。定理証明ツールは手動で書かれた証明スクリプトによってシステムソフトウェアの機能の正確さを検証し、この検証方式の表現力が強く、複雑なシステムを証明できるが、自動化程度が低く、検証コストが比較的高い。一方,プログラム検証器を用いて,標準コードを生成するためのソースコードを用いて検証条件を生成し,検証条件を制約ソルバに自動的に解くことにより,複雑なシステムソフトウェアのすべての機能の正確さを検証することは難しい。............................................の自動的な解を求めることは難しい.上記の2つの方式の利点を結合して,Coqにおける制約付きソルバZ3を自動的に証明することによって,自動的に証明される程度を向上させるために,Coqにおいて自動的に証明される方式を提案した。それは,ユーザの手動検証プログラムのコストを減少させることができた。Data from Wanfang. Translated by JST【JST・京大機械翻訳】

シソーラス用語： プログラム検証 ,  *システムプログラム ,  定理証明 ,  自動化
準シソーラス用語： ソルバ ,  ソースコード ,  表現力 ,  スクリプト ,  ソフトウェアシステム ,  形式的検証 , 【Automatic Indexing@JST】

著者キーワード (5件)： formal verification ,  proof assistant tool ,  SMT solver ,  Coq ,  Z3

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： 証明 ,  戦略 ,  設計