An Algorithm for Checking PL/CV Arithmetic Inferences
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.
computer science; technical report
Previously Published As