Top > Search of International Patents > PROGRAM VERIFICATION DEVICE, PROGRAM VERIFICATION METHOD, COMPUTER PROGRAM FOR PROGRAM VERIFICATION, PROGRAM CONVERTER, PROGRAM CONVERSION METHOD, COMPUTER PROGRAM FOR PROGRAM CONVERSION, PROGRAM MANUFACTURING METHOD, AND PROGRAM FOR VERIFICATION

PROGRAM VERIFICATION DEVICE, PROGRAM VERIFICATION METHOD, COMPUTER PROGRAM FOR PROGRAM VERIFICATION, PROGRAM CONVERTER, PROGRAM CONVERSION METHOD, COMPUTER PROGRAM FOR PROGRAM CONVERSION, PROGRAM MANUFACTURING METHOD, AND PROGRAM FOR VERIFICATION

Foreign code F200010067
File No. 6016
Posted date May 15, 2020
Country WIPO
International application number 2018JP044029
International publication number WO 2019124022
Date of international filing Nov 29, 2018
Date of international publication Jun 27, 2019
Priority data
  • P2017-246154 (Dec 22, 2017) JP
Title PROGRAM VERIFICATION DEVICE, PROGRAM VERIFICATION METHOD, COMPUTER PROGRAM FOR PROGRAM VERIFICATION, PROGRAM CONVERTER, PROGRAM CONVERSION METHOD, COMPUTER PROGRAM FOR PROGRAM CONVERSION, PROGRAM MANUFACTURING METHOD, AND PROGRAM FOR VERIFICATION
Abstract A program verification device 10 comprising a converter 20 for generating a converted program subject to formal verification, said converted program including a fused loop statement wherein a plurality of loop statements included in an original program have been fused.
Outline of related art and contending technology BACKGROUND ART
The program verify operation as described in the specification of the technique, referred to as a program verify operation. Program verification, the certificate without executing the program, the validity of the program in the formal techniques to verify the mathematical formal verification is used.
Non-Patent Document 1 is, functionally equivalent to a given program is a program for generating a simple invariant condition to the program conversion method is disclosed. Can be made simple and invariant conditions, can be verified at high speed. Non-Patent Document 1 is, the program generated by the conversion program verify is disclosed, the program Loop Fusion does not disclose to verify.
Non-Patent Document 2 is, loop fusion is disclosed. Loop fusion, a plurality of loops included in a single sentence in the fuzed loop statement. Conventional, loop fusion, has been used for compiler optimization is, the program verification is not used.
Scope of claims (In Japanese)[請求項1]
 形式的検証の対象となる変換プログラムであって、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成する変換器
 を備えるプログラム検証装置。

[請求項2]
 前記変換プログラムは、複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名が変更されている
 請求項1に記載のプログラム検証装置。

[請求項3]
 前記変換プログラムは、前記変換プログラムを、前記形式的検証の対象として、前記オリジナルプログラムと等価にするステートメントを含む
 請求項2に記載のプログラム検証装置。

[請求項4]
 前記変換プログラムは、
  前記変換プログラムが可能である実行を列挙するための第1ステートメントと、
  前記第1ステートメントによって列挙された実行のうち、前記オリジナルプログラムが可能な実行に対応するものを、前記形式的検証の対象にするための第2ステートメントと、
 を含む請求項2に記載のプログラム検証装置。

[請求項5]
 前記変換プログラムは、
  前記融合ループ文の前に設けられた第1ステートメントと、
  前記融合ループ文の後に設けられた第2ステートメントと、
をさらに含み、
 前記第1ステートメントは、所定の変数が、前記融合ループ文の実行後にとり得る値を非決定的に列挙するステートメントであり、
 前記第2ステートメントは、前記融合ループ文の実行後において前記所定の変数がとる値が、前記第1ステートメントによって非決定的に列挙された前記値と等価である場合を、前記形式的検証の対象にするステートメントである
 請求項2に記載のプログラム検証装置。

[請求項6]
 前記変換器は、複数の前記ループ文の少なくとも一つの対象ループ文を、前記対象ループ文の逆実行ループ文に変換し、前記対象ループ文に代えて前記逆実行ループ文を含む複数のループ文をループ融合する
 請求項1~5のいずれか1項に記載のプログラム検証装置。

[請求項7]
 前記変換プログラムは、前記逆実行ループ文を、前記形式的検証の対象として、前記対象ループ文と等価にするステートメントを含む
 請求項6に記載のプログラム検証装置。

[請求項8]
 オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成して記憶部に記憶させ、
 プログラムを形式的検証する検証器によって、前記記憶部に記憶された前記変換プログラムを形式的検証する
 ことを含むプログラム検証方法。

[請求項9]
 コンピュータに、プログラム検証処理を実行させるコンピュータプログラムであって、
前記プログラム検証処理は、
  オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、
  前記変換プログラムを形式的検証する
 ことを含む、プログラム検証のためのコンピュータプログラム。

[請求項10]
 オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成するプログラム変換器であって、
 複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更するよう構成されている
 プログラム変換器。

[請求項11]
 プログラム変換器が、記憶部に記憶されたオリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、
 前記プログラム変換器が、変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成する
 ことを含むプログラム変換方法。

[請求項12]
 コンピュータに、プログラム変換処理を実行させるコンピュータプログラムであって、
前記プログラム変換処理は、
  オリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、
  変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成する
 ことを含む、プログラム変換のためのコンピュータプログラム。

[請求項13]
 オリジナルプログラムを作成し、
 前記オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、
 プログラムを形式的検証する検証器によって、前記変換プログラムを形式的検証し、
 前記形式的検証の結果に基づいて、前記オリジナルプログラムを修正する
 ことを含むプログラムの製造方法。

[請求項14]
 プログラムを形式的検証する検証器によって検証される検証用プログラムであって、
 オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を有する
 検証用プログラム。
  • Applicant
  • ※All designated countries except for US in the data before July 2012
  • KYOTO UNIVERSITY
  • Inventor
  • SUENAGA Kohei
  • IMANISHI Akifumi
  • IGARASHI Atsushi
IPC(International Patent Classification)
Specified countries National States: AE AG AL AM AO AT AU AZ BA BB BG BH BN BR BW BY BZ CA CH CL CN CO CR CU CZ DE DJ DK DM DO DZ EC EE EG ES FI GB GD GE GH GM GT HN HR HU ID IL IN IR IS JO KE KG KH KN KP KR KW KZ LA LC LK LR LS LU LY MA MD ME MG MK MN MW MX MY MZ NA NG NI NO NZ OM PA PE PG PH PL PT QA RO RS RU RW SA SC SD SE SG SK SL SM ST SV SY TH TJ TM TN TR TT TZ UA UG US UZ VC VN ZA ZM ZW
ARIPO: BW GH GM KE LR LS MW MZ NA RW SD SL SZ TZ UG ZM ZW
EAPO: AM AZ BY KG KZ RU TJ TM
EPO: AL AT BE BG CH CY CZ DE DK EE ES FI FR GB GR HR HU IE IS IT LT LU LV MC MK MT NL NO PL PT RO RS SE SI SK SM TR
OAPI: BF BJ CF CG CI CM GA GN GQ GW KM ML MR NE SN ST TD TG
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