Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

https://hal.inria.fr/inria-00525129
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 11:43:35 AM
Last modification on : Monday, October 11, 2010 - 11:43:35 AM

Identifiers

  • HAL Id : inria-00525129, version 1

Collections

Citation

Alexksandar Dimovski. A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.121-135. ⟨inria-00525129⟩

Share

Metrics

Record views

15