Top > Search of Japanese Patents > AUTOMATIC CERTIFICATION DEVICE AND PROGRAM

AUTOMATIC CERTIFICATION DEVICE AND PROGRAM

Patent code P200016800
File No. 5771
Posted date May 8, 2020
Application number P2017-137949
Publication number P2019-020966A
Date of filing Jul 14, 2017
Date of publication of application Feb 7, 2019
Inventor
  • (In Japanese)蓮尾 一郎
  • (In Japanese)奥殿 貴仁
  • (In Japanese)木戸 肩吾
  • (In Japanese)末永 幸平
  • (In Japanese)小島 健介
  • (In Japanese)西田 雄気
Applicant
  • (In Japanese)国立大学法人東京大学
  • (In Japanese)国立大学法人京都大学
Title AUTOMATIC CERTIFICATION DEVICE AND PROGRAM
Abstract PROBLEM TO BE SOLVED: To provide an automatic certification device and a program capable of facilitating interpretation of a real certification object corresponding to an obtained interpolation.
SOLUTION: An automatic certification device receives an input from a solver that generates and outputs a polynomial equation representing Craig interpolation for a given certification object; obtains approximate coefficients approximated so that a ratio of coefficients included in the polynomial equation is an integer ratio and a value corresponding to each coefficient is a smaller value; selects an approximate coefficient in an order determined by a predetermined method from among the obtained approximate coefficients, and generates a trial polynomial equation in which coefficients of the received polynomial equation are replaced with the selected approximate coefficients; and verifies whether the trial polynomial equation is established as the polynomial equation representing the Craig interpolation.
Outline of related art and contending technology (In Japanese)

近年、大規模集積回路(LSI)等の、ハードウェアの設計や検証、ソフトウェアプログラムの検証等において、人為的介入なしに自動で推論を行う自動証明装置の利用が検討されている。例えば、非特許文献2には、ハードウェア設計を、クレイグ補間を用いた方法で検証を行うことで、検証可能な対象を広げることができることが開示されている。

こうした研究を受けて、与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーが開発されている(例えば非特許文献1)。このようなソルバーにおいては、多項式の係数が、数値解析により得られているので、一般に簡潔な整数比としては表現されない。また、当該係数には数値誤差を含む。

Field of industrial application (In Japanese)

本発明は、自動証明装置、及びプログラムに関する。

Scope of claims (In Japanese)
【請求項1】
 
与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる手段と、
前記受け入れた多項式に含まれる係数の比が、整数の比となり、かつ各係数に対応する値がより小さい値となるよう近似した近似係数を、複数求める係数演算手段と、
前記複数求められた近似係数のうちから、予め定めた方法で決定された順に近似係数を選択し、前記受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する検証手段と、
前記検証により、前記求めたいずれかの近似係数に基づく前記試行多項式が、前記クレイグ補間を表す多項式として成立すると、前記検証手段により判断されたときに、当該近似係数を、解として生成する生成手段と、
を含み、
前記生成手段は、前記求めたいずれかの近似係数に基づく前記試行多項式が、いずれも前記クレイグ補間を表す多項式として成立しないとして前記検証手段により判断されたときには、エラーが発生したものとして所定の処理を実行する、
自動証明装置。

【請求項2】
 
請求項1記載の自動証明装置であって、
前記ソルバーは、前記証明対象に係る制約が、
任意の変数値に対して
0以上である多項式f、
0より大である多項式g、
0に等しい多項式h
のいずれかを少なくとも一つ含んで設定され、
一対の制約T,T′のクレイグ補間を表す多項式を生成して出力するソルバーである自動証明装置。

【請求項3】
 
請求項1または2に記載の自動証明装置であって、
前記出力される解が、プログラム検証または定理証明の処理に供される自動証明装置。

【請求項4】
 
請求項1に記載の自動証明装置であって、
前記ソルバーは、前記証明対象に係る制約が、
任意の変数値に対して
0以上である多項式f、
0に等しくない多項式g、
0に等しい多項式h
のいずれかを少なくとも一つ含んで設定され、
一対の制約T,T′のクレイグ補間を表す多項式を生成して出力するソルバーである自動証明装置。

【請求項5】
 
コンピュータを、
与えられた証明対象に係るクレイグ補間を表す多項式を生成して出力するソルバーからの入力を受け入れる手段と、
前記受け入れた多項式に含まれる係数の比が、整数の比となり、かつ各係数に対応する値がより小さい値となるよう近似した近似係数を、複数求める係数演算手段と、
前記複数求められた近似係数のうちから、予め定めた方法で決定された順に近似係数を選択し、前記受け入れた多項式の係数を当該選択した近似係数に置き換えた試行多項式を生成し、当該試行多項式が、前記クレイグ補間を表す多項式として成立するかを検証する検証手段と、
前記検証により、前記求めたいずれかの近似係数に基づく前記試行多項式が、前記クレイグ補間を表す多項式として成立すると、前記検証手段により判断されたときに、当該近似係数を解として生成し、前記求めたいずれかの近似係数に基づく前記試行多項式が、いずれも前記クレイグ補間を表す多項式として成立しないとして前記検証手段により判断されたときには、エラーが発生したものとして所定の処理を実行する生成手段と、
として機能させるプログラム。
IPC(International Patent Classification)
F-term
Drawing

※Click image to enlarge.

JP2017137949thum.jpg
State of application right Published
Please contact us by e-mail or facsimile if you have any interests on this patent. Thanks.


PAGE TOP

close
close
close
close
close
close
close