IOP: The InterOperability Platform & IMaude: An Interactive Extension of Maude

We describe a platform, IOP, for the interoperation of formal reasoning tools, and an adaptation of Maude, IMaude, that utilizes this platform. Three applications of IMaude and IOP to real world problem domains are described.