Abstract: Compositional verification is a promising approach to alleviate the state-explosion problem of Model Checking. The basic idea behind this approach is divide-and-conquer: it utilizes an Assume-Guarantee rule to decompose a verification task into smaller subtasks and verify each subtask individually.

The major difficulty in using an Assume-Guarantee rule to do a decomposition is to search for appropriate contextual assumptions; the search usually requires human intervention. In the past five years, several approaches based on machine learning techniques have been proposed to automate the Assume-Guarantee style of composition verification under an automata theoretical framework.

In this talk, I will explain learning-based automated compositional verification approaches and discuss their common problems: (1) Most of the approaches are heuristics in the sense that they cannot guarantee finding the best contextual assumption. (2) All of the algorithms have been proposed so far are explicit state approaches; they explicitly construct the complete transition systems of the contextual assumptions. (3) they cannot handle liveness properties, which are essential to verify the correctness of a system. These problems are important and fundamental because they are originated from the L* learning algorithm, which is the core of the mainstream learning-based automated compositional verification approaches. I will also discuss solutions to some of these problems and their preliminary experimental results.

Yu-Fang Chen is a PhD candidate at National Taiwan University. His research interests include Model Checking, machine learning, automata theory, software verification, and formal methods. He is involved in the iCAST project. Appointments: dcm@cs.cmu.edu