Compositional Verification

A key step in achieving scalability in the verification of
large software systems is to "divide and conquer"; that is, to break up the verification of a system into smaller tasks that
involve the verification of its components. Assume-guarantee reasoning is a widespread divide-and-conquer approach that uses assumptions as it checks individual components of a system. Assumptions essentially encode expectations that each component has from the rest the system in order to operate correctly. Coming up with the right assumptions is typically a non-trivial manual process, which limits the applicability of this type of reasoning in practice. Over the last few years, the RSE group has developed a collection of techniques and a supporting toolset for performing assume-guarantee reasoning of software in an automated fashion. The techniques are applicable both at the level of design models and at the level of actual source code. Assumptions are computed automatically, using two main approaches: the first, which received an ACM distinguished paper award in 2002, computes the assumption based on the specification of the component and a required property; the second learns the assumption through queries and counterexamples.

*Reviewed 2012*