Using Machine Learning to Verify Systems

Automated verification of software systems is a challenging problem because of their large (and often infinite) state-space. In this talk, we explore techniques from computational learning theory for verification of such systems. We show that learning can be effectively used to verify safety properties as well as liveness properties with fairness constraints. We can analyze both linear time and branching time temporal logics (more precisely omega-regular properties and Computational Tree Logic). We represent the states of the system as strings over some alphabet and use Angluin’s algorithm for learning regular sets. We show that the learning based verification procedure is sound and, more interestingly, also complete if the fixpoints needed for verification are in fact regular. Finally, we conclude with discussion about a tool called LEVER which implements these techniques and some examples that we have analyzed using the tool.