Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### viernes 4 de enero de 2013

10:45am Meeting room 302 (Mountain View), level 3

**Aleksandar Dimovski***, PhD Student**, FON University, Macedonia*

### Program Verification by Game Semantics: From Abstraction-Refinement to Symbolic Approach

#### Abstract:

Game semantics is a denotational semantics which constructs models of terms
(open programs) by looking at the ways in which a term can observably interact
with its environment. The obtained models are fully abstract (sound and
complete), and are the most accurate models we can find for a programming
language. Game semantics models can be given certain kinds of concrete
automata-theoretic representations for several interesting language fragments
with finite data types, and so they can serve as a basis for software model
checking and program analysis. Here we examine several techniques for automatic
verification of safety properties of terms with infinite data types.
We have developed an abstraction-refinement procedure, which starts by
model-checking the most abstract version of the concrete program. If no
counterexample or a genuine one is found, the procedure terminates. Otherwise,
it uses a spurious counterexample to gradually refine the abstraction for the
next iteration.
We can combine this approach with a method for verifying data-independent terms.
We say that a term is data-independent with respect to a data type X, if the
only operation available on values of type X is the equality test. We provide
results which reduce the verification of some properties for all interpretations
of X, to the verification for finite interpretations of X.
Finally, we present a new symbolic approach for representing game semantics
models, and show how it can be applied for efficient verification of terms. By
using symbolic values instead of concrete ones, we generalize the standard
notion of automata representation of game semantics to that of symbolic-automata
representation. In this way terms with infinite data types can be expressed as
finite-state symbolic-automata, and so various properties can be checked over
them.