Learning Minimal Requirements for Compositional Verification
Arnaud Fietzke
Compositional verification is a technique aimed at addressing the state explosion problem associated with model checking. One approach to compositional verification is assume-guarantee reasoning, in which the verification of components of a system allows properties of the whole system to be checked by using assumptions derived from one component in the verification of a second component. Once such intermediate assumptions have been found, they can be used to re-run the verification of the whole system at much lower computational expense. In this context, the size of the intermediate assumptions is of primary importance.
In this thesis we discuss a method for computing minimal intermediate assumptions. The method is based on a recent approach to automatic derivation of intermediate assumptions using the L* algorithm for active learning of regular languages.
Bachelor Thesis.