Program verification using symbolic game semantics

Aleksandar Dimovski

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review


We introduce a new symbolic representation of algorithmic game semantics, and show how it can be applied for efficient verification of open (incomplete) programs. The focus is on an Algol-like programming language which contains the core ingredients of imperative and functional languages, especially on its second-order recursion-free fragment with infinite data types. We revisit the regular-language representation of game semantics of this language fragment.
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.
Original languageEnglish
Article number560
JournalTheoretical Computer Science
Issue number3
Pages (from-to)364
Number of pages379
Publication statusPublished - 16 Jan 2014


  • Algorithmic Game Semantics
  • Symbolic Automata
  • Program Verification
  • Predicate Abstraction


Dive into the research topics of 'Program verification using symbolic game semantics'. Together they form a unique fingerprint.

Cite this