ITU

Program verification using symbolic game semantics

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

View graph of relations

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
Volume560
Issue number3
Pages (from-to)364
Number of pages379
ISSN0304-3975
DOIs
Publication statusPublished - 16 Jan 2014
Close

    Research areas

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

Downloads

No data available

ID: 79312582