Symbolic Execution of the Gist Specification Language

Abstract

Symbolic execution can help clarify the behavior implied by a program specification without implementing that specification, and can thereby assist the difficult process of developing a correct specification. However, symbolic execution of specifications poses problems that do not arise in symbolic execution of ordinary programming languages. We describe a symbolic evaluator, named KOKO, for the Gist specification language, and show how it copes with such high-level constructs as nondeterminism, constraints, and reference by description.

Cite

Text

Cohen. "Symbolic Execution of the Gist Specification Language." International Joint Conference on Artificial Intelligence, 1983.

Markdown

[Cohen. "Symbolic Execution of the Gist Specification Language." International Joint Conference on Artificial Intelligence, 1983.](https://mlanthology.org/ijcai/1983/cohen1983ijcai-symbolic/)

BibTeX

@inproceedings{cohen1983ijcai-symbolic,
  title     = {{Symbolic Execution of the Gist Specification Language}},
  author    = {Cohen, Donald},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1983},
  pages     = {17-20},
  url       = {https://mlanthology.org/ijcai/1983/cohen1983ijcai-symbolic/}
}