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.
© 2010 Microsoft Corporation. All rights reserved.
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.