Heuristic methods for mechanically deriving inductive assertio
Ben Hegbreitt · International Joint Conference on Artificial Intelligence · 1973
Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error-prone, producing a program with complete, correct predicates is reasonably difficult and would be facilitated by machine assistance. This paper discusses heuristic methods for mechanically deriving loop predicates from their boundary conditions and for mechanically completing partially specified loop predicates.