A Heuristic Approach to Program Verification
Abstract
We present various heuristic techniques for use in proving the correctness of computer programs. The techniques are designed to obtain automatically the assertions attached to the loops of the program which previously required human understanding of the program''s performance. We distinguish between two general approaches: one in which we obtain the inductive assertion by analyzing predicates which are known to be true at the entrances and exits of the loop ($underline{top-down}$ approach), and another in which we generate the inductive assertion directly from the statements of the loop ($underline{bottom-up}$ approach).
Cite
Text
Katz and Manna. "A Heuristic Approach to Program Verification." International Joint Conference on Artificial Intelligence, 1973.Markdown
[Katz and Manna. "A Heuristic Approach to Program Verification." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/katz1973ijcai-heuristic/)BibTeX
@inproceedings{katz1973ijcai-heuristic,
title = {{A Heuristic Approach to Program Verification}},
author = {Katz, Shmuel and Manna, Zohar},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1973},
pages = {500-512},
url = {https://mlanthology.org/ijcai/1973/katz1973ijcai-heuristic/}
}