An Algorithm for Checking PL/CV Arithmetic Inferences
Tat Y. Chan · eCommons (Cornell University) · 1977
This paper describes the operation and implementation of the arithmetic proof rule for the quantifier free integer arithmetic used in the PL/CV 2 program verification system. The general arithmetic satisfiability problem underlying the rule is shown to be NP complete.