Top > Search of Japanese Patents > INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD

INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD UPDATE_EN meetings

Patent code P180015679
File No. 5295
Posted date Nov 22, 2018
Application number P2016-017441
Publication number P2017-138679A
Patent number P6632058
Date of filing Feb 1, 2016
Date of publication of application Aug 10, 2017
Date of registration Dec 20, 2019
Inventor
  • (In Japanese)末永 幸平
  • (In Japanese)樹下 稔
  • (In Japanese)小島 健介
Applicant
  • (In Japanese)国立大学法人京都大学
Title INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD UPDATE_EN meetings
Abstract PROBLEM TO BE SOLVED: To provide a novel technique for generating invariants.
SOLUTION: An invariant generator 100 includes a storage unit 300 having a program code stored therein, and a processing unit 200 for executing invariant generation processing. The processing unit 200 executes a third process for generating an invariant. The third process includes; a matrix generation process for generating a representation matrix, which is a transpose of a transformation matrix representing transformation of each of one or more sub-expressions made by execution of a program code; an arithmetic process for deriving an eigenvalue and eigenvector of the representation matrix; and an invariant generation process for generating an invariant based on a set of eigenvalue and eigenvector and the one or more sub-expressions.
Outline of related art and contending technology (In Japanese)

不変条件(Invariant)は、プログラムコード(以下、単に「コード」ということがある)の形式的検証(formal verification)に用いられる。形式的検証は、プログラムコードの正当性を数学的な形式的手法で証明することである。プログラムコードに含まれるある処理に対する不変条件は、その処理の実行前後において成立する条件として構成される。while文のようなループ処理に対する不変条件は、ループ不変条件(Loop Invariant)と呼ばれる。ループ不変条件は、ループの開始時点で成立するとともに、ループを何回繰り返しても成立する条件として構成される。

不変条件を生成する従来の方法には、非特許文献1等に記載のテンプレート法(template-based method)がある。テンプレート法では、多項式pが、不変条件に関係するテンプレートとして生成される。多項式pは、検証対象のプログラムコードに含まれるシンボルと不定係数によって構成される。シンボルとは、プログラムに含まれる変数又は定数を示す文字又は記号である。そして、p=0が不変条件であるような制約が生成される。この制約を解析することで、不変条件が得られる。

Field of industrial application (In Japanese)

本発明は、不変条件生成装置等に関するものである。

Scope of claims (In Japanese)
【請求項1】
 
不変条件生成装置であって、
プログラムコードが記憶される記憶部と、
前記不変条件を生成する処理を実行する処理部を備え、
前記処理は、
前記記憶部から前記プログラムコードを読み出す第1処理と、
多項式を構成するための1又は複数の部分式を生成する第2処理と、
前記不変条件を生成する第3処理と、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記不変条件を生成する不変条件生成処理と、
を含む
不変条件生成装置。

【請求項2】
 
前記表現行列の一つの固有値に対して複数の独立な固有ベクトルが存在する場合には、
前記不変条件生成処理は、複数の固有ベクトルの線形結合を、前記不変条件の生成に用いる
請求項1記載の不変条件生成装置。

【請求項3】
 
1又は複数の前記部分式それぞれの前記変換が、前記変換行列だけでなく余りベクトルによっても表される場合には、
前記不変条件生成処理は、前記固有ベクトルと前記余りベクトルとの内積が0になる条件の下で前記不変条件を生成する
請求項1又は2記載の不変条件生成装置。

【請求項4】
 
請求項1~3のいずれか1項に記載の不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラム。

【請求項5】
 
不変条件を生成する処理を実行する処理部によって実行される方法であって、
記憶部からプログラムコードを読み出す第1処理を実行すること、
多項式を構成するための1又は複数の部分式を生成する第2処理を実行すること、
前記不変条件を生成する第3処理を実行すること、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記不変条件を生成する不変条件生成処理と、
を含む
方法。

【請求項6】
 
プログラムコードを作成すること、
請求項5に記載の前記記憶部が、作成されたプログラムコードを記憶すること、
請求項5に記載の方法によって、前記プログラムコードの不変条件を生成すること、
前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、
前記形式的検証の結果に基づいて前記プログラムコードを修正すること、
を含むプログラムコードの製造方法。
IPC(International Patent Classification)
F-term
Drawing

※Click image to enlarge.

JP2016017441thum.jpg
State of application right Registered
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