A Heuristic Approach to Program Verification

Katz, Shmuel; Manna, Zohar

A Heuristic Approach to Program Verification

Download BibTeX Cite

Proceedings of the Third International Joint Conference on Artificial Intelligence. Automatic Programming. Pages 500-511.

Abstract

We present various heuristic techniques for use in proving the correctness of computer programs. The techniques are designed to obtain automatically the "inductive 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 (top-down approach), and another in which we generate the inductive assertion directly from the statements of the loop (bottom-up approach).

Shmuel Katz, and Zohar Manna. 1973. A Heuristic Approach to Program Verification. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73. IJCAI, 500–511. https://ijcai.org/proceedings/1973/64

@inproceedings{ijcai1973p64,
  title     = {A Heuristic Approach to Program Verification},
  author    = {Katz, Shmuel and Manna, Zohar},
  booktitle = {Proceedings of the Third International Joint Conference on
               Artificial Intelligence, {IJCAI-73}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Nils J. Nilsson},
  pages     = {500--511},
  year      = {1973},
  month     = {8},
  note      = {Automatic Programming},
  url       = {https://ijcai.org/proceedings/1973/64},
}

TY  - CPAPER
TI  - A Heuristic Approach to Program Verification
AU  - Katz, Shmuel
AU  - Manna, Zohar
T2  - Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1973
SP  - 500
EP  - 511
UR  - https://ijcai.org/proceedings/1973/64
ER  -