TOP > 外国特許検索 > 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

外国特許コード F200010067
整理番号 6016
掲載日 2020年5月15日
出願国 世界知的所有権機関(WIPO)
国際出願番号 2018JP044029
国際公開番号 WO 2019124022
国際出願日 平成30年11月29日(2018.11.29)
国際公開日 令和元年6月27日(2019.6.27)
優先権データ
  • 特願2017-246154 (2017.12.22) JP
発明の名称 (英語) 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
発明の概要(英語) 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.
従来技術、競合技術の概要(英語) 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.
  • 出願人(英語)
  • ※2012年7月以前掲載分については米国以外のすべての指定国
  • KYOTO UNIVERSITY
  • 発明者(英語)
  • SUENAGA Kohei
  • IMANISHI Akifumi
  • IGARASHI Atsushi
国際特許分類(IPC)
指定国 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
ライセンスをご希望の方、特許の内容に興味を持たれた方は、下記までご連絡ください。

PAGE TOP

close
close
close
close
close
close