Program verification using symbolic game semantics
Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review
By using symbolic values instead of concrete ones, we generalize the standard notions of regular-language and automata representations of game semantics to that of corresponding symbolic representations. In this way programs with infinite data types, such as integers, can be expressed as finite-state symbolic-automata although the standard automata representation is infinite-state, i.e. the standard regular-language representation has infinite summations. Moreover, in this way significant reductions of the state space of game semantics models are obtained. This enables efficient verification of programs by our prototype tool based on symbolic game models, which is illustrated with several examples.
- Algorithmic Game Semantics , Symbolic Automata , Program Verification , Predicate Abstraction