Feb 08, 2011: Lesley Wevers: Learning for Compositional Verification

February 08, 2011Learning for Compositional Verification
Room: Zi 5126Lesley Wevers

Assume-guarantee reasoning enables a divide-and-conquer approach to the verification of large systems by checking system components separately using assumptions about the environment of each component. Finding assumptions can be done by hand, but this is a time consuming process. In this talk I'm presenting a paper by Corina S. Pasareanu et al., which describes a framework for performing assume-guarantee reasoning on a system in a fully automatic fashion. The framework uses an off-the-shelf learning algorithm to iteratively compute assumptions which are approximate at first, but guiding the algorithm by analyzing counter-examples enables the assumptions to become more precise. In this presentation I will be covering assume-guarantee reasoning, applying the L* algorithm to perform automatic assume-guarantee reasoning, alphabet-refinement to reduce the size of the learned assumptions, and I will conclude with some experimental results.