Abstract: A solution for program polynomial invariant generation problem is presented. An iteration upper approximation method that was successfully applied on free algebras in this paper was adopted for polynomial ring. Set of invariants is interpreted as an ideal over polynomial ring. Relationship and intersection problems solution are proposed. Intersection of Gröbner basis is applied to solve intersection problem. Inverse obligatory is applied to solve relationship problem.

Keywords: verification theory, invariant generation, polynomial ring.

ACM Classification Keywords: D.2.4 Software/Program Verification: Assertion checkers; F.3.1 Specifying and Verifying and Reasoning about Programs: Invariants; I.2.2 Automatic Programming: Program verification; B.6.3 Design Aids : Verification; D.4.5 Reliability: Verification.

Link:

Program Invariants Generation over Polynomial Ring using Iterative Methods.

Sergii Kryvyi, Oleksandr Maksymets

http://www.foibg.com/ijita/vol20/ijita20-02-p02.pdf