A Simplifier for Program Verification with Built-in Knowledge on Equality and Partial Ordering and its Use for Finding Loop Invariants

スポンサーリンク

概要

• 論文の詳細を見る

• This paper describes a simplification and deduction procedure on equality and partial ordering theory, as well as its implementation. It also deals with the problem of finding loop invariants for program verification, making use of the simplification capability. Simplifier based on this procedure is a component of VFPL Verifier, a problem-oriented verifier that deals with file processing programs. The method makes use of graph processing technique. Its characteristics are: i) efficient, especially for handling theorems for program verification; ii)relatively simple and easy to implement; iii)possible to treat both < and &le; relations explicitly.

• 一般社団法人情報処理学会の論文
• 1984-02-05

著者

• Tamai Tetsuo

  Mitsubishi Research Institute Inc.

• TAMAI TETSUO

  Mitsubishi Research Institute, Inc.

関連論文

• A Simplifier for Program Verification with Built-in Knowledge on Equality and Partial Ordering and its Use for Finding Loop Invariants
• A Verification System for File Processing Programs (Mathematical Methods in Software Science and Engineering : Third Conference)

スポンサーリンク