A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs

Abstract : In this paper we address the problem of deciding may- and must-equivalence and termination of nondeterministic finite programs from second-order recursion-free Erratic Idealized Algol. We use game semantics to compositionally extract finite models of programs, and the CSP process algebra as a concrete formalism for representation of models and their efficient verification. Observational may- and must-equivalence and liveness properties, such as divergence and termination, are decided by checking traces renements and divergence-freedom of CSP processes using the FDR tool. The practicality of the approach is evaluated on several examples.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.121-135, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525129
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 11:43:35
Dernière modification le : lundi 11 octobre 2010 - 11:43:35

Identifiants

  • HAL Id : inria-00525129, version 1

Collections

Citation

Alexksandar Dimovski. A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.121-135, 2010, Lecture Notes in Computer Science. 〈inria-00525129〉

Partager

Métriques

Consultations de la notice

12