Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Alternating Simulation and IOCO

Margus Veanes and Nikolaj Bjorner


We propose a symbolic framework called guarded labeled assignment systems or GLASs and show how GLASs can be used as a foundation for symbolic analysis of various aspects of formal specification languages. We define a notion of i/o-refinement over GLASs as an alternating simulation relation and provide formal proofs that relate i/o-refinement to ioco. We show that non-i/o-refinement reduces to a reachability problem and provide a translation from bounded non-i/o-refinement or bounded non-ioco to checking first-order assertions.


Publication typeTechReport
PublisherMicrosoft Research

Newer versions

Margus Veanes and Nikolaj Bjorner. Alternating Simulation and IOCO, Springer Verlag, November 2010.

Margus Veanes and Nikolaj Bjorner. Alternating simulation and IOCO, International Journal on Software Tools for Technology Transfer (STTT) , Springer, November 2011.

> Publications > Alternating Simulation and IOCO