Verifying Data Independent Programs Using Game Semantics

Abstract : We address the problem of verification of program terms parameterized by a data type X, such that the only operations involving X a program can perform are to input, output, and assign values of type X, as well as to test for equality such values. Such terms are said to be data independent with respect to X. Logical relations for game semantics of terms are defined, and it is shown that the Basic Lemma holds for them. This proves that terms are predicatively parametrically polymorphic, and it provides threshold collections, i.e. sufficiently large finite interpretations of X, for the problem of verification of observational-equivalence, approximation, and safety of parameterized terms for all interpretations of X. In this way we can verify terms with data independent infinite integer types. The practicality of the approach is evaluated on several examples.
Type de document :
Communication dans un congrès
Walter Binder; Eric Bodden; Welf Löwe. 12th International Conference on Software Composition (SC), Jun 2013, Budapest, Hungary. Springer, Lecture Notes in Computer Science, LNCS-8088, pp.128-143, 2013, Software Composition. 〈10.1007/978-3-642-39614-4_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01492794
Contributeur : Hal Ifip <>
Soumis le : lundi 20 mars 2017 - 15:40:13
Dernière modification le : mardi 16 janvier 2018 - 15:43:54
Document(s) archivé(s) le : mercredi 21 juin 2017 - 13:24:13

Fichier

978-3-642-39614-4_9_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Aleksandar Dimovski. Verifying Data Independent Programs Using Game Semantics. Walter Binder; Eric Bodden; Welf Löwe. 12th International Conference on Software Composition (SC), Jun 2013, Budapest, Hungary. Springer, Lecture Notes in Computer Science, LNCS-8088, pp.128-143, 2013, Software Composition. 〈10.1007/978-3-642-39614-4_9〉. 〈hal-01492794〉

Partager

Métriques

Consultations de la notice

23

Téléchargements de fichiers

5