On the equivalence-checking problem for polysemantic models of sequential programs.

On the equivalence-checking problem for polysemantic models of sequential programs.

I.M. Zakharyaschev, V.A. Zakharov.

Abstract

We introduce a new propositional model of computation for sequential computer programs. A distinctive feature of this model is that program runs and the results of computations are defined by means of two independent operational semantics. One of them can be regarded as an internal semantics that is used for routing runs in the control-flow graph of a program. The other one can be viewed as an observational semantics which is used for interpreting the results of a program execution. We show that some conventional models of sequential and recursive programs can be embedded into our model. We consider the equivalence-checking problem for the presented model and develop a uniform approach to the design of efficient equivalence-checking algorithms.

Edition

Proceedings of the Institute for System Programming, vol. 6 (in Russian), 2004, Стр. 179-198.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

For citation

I.M. Zakharyaschev, V.A. Zakharov. On the equivalence-checking problem for polysemantic models of sequential programs. . Proceedings of the Institute for System Programming, vol. 6 (in Russian), 2004, Стр. 179-198. .

Full text of the paper in pdf (in Russian) Back to the contents of the volume