Program verification using symbolic game semantics

Aleksandar Dimovski

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

Abstract

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.
OriginalsprogEngelsk
Artikelnummer560
TidsskriftTheoretical Computer Science
Vol/bind560
Udgave nummer3
Sider (fra-til)364
Antal sider379
ISSN0304-3975
DOI
StatusUdgivet - 16 jan. 2014

Fingeraftryk

Dyk ned i forskningsemnerne om 'Program verification using symbolic game semantics'. Sammen danner de et unikt fingeraftryk.

Citationsformater