CoPS is an automatic checker of multilevel system security properties. CoPS can be used to check three different bisimulation-based non-interference properties for systems expressed as terms of the Security Process Algebra (SPA) language. The considered properties are persistent, in the sense that they are preserved at each execution step. Moreover, they imply the Bisimulation-based Non Deducibility on Composition (BNDC) property, whose decidability is still an open problem.
