Compositional verification using interface recognizers/suppliers (IRS)

In this thesis, we review recent developments in compositional and assume guarantee verification. We discuss whether each method supports circular/non circular reasoning and whether it can be used when proving safety/liveness properties.; We formulate interface recognizers/suppliers (IRS), which are recognizers augmented with Boolean constraints. The constraints specify what values may occur on IRS inputs at each state. In other words, IRS can constrain its inputs.; We discuss a composition theorem for circular reasoning using IRS. In this way, IRS framework extends non-circular constraint model checking [25] to a circular constrainted model checking.; We demonstrate an application of IRS in (1) specifying environment assumptions and in (2) modeling pre conditions/post conditions of properties of an ATM switch. Using IRS, we specify and then verify the switch.