Learning to Verify Systems

Making high quality and reliable software systems remains a difficult problem. One approach to address this problem is automated verification which attempts to demonstrate algorithmically that a software system meets its specification. However, verification of software systems is not easy: such systems are often modeled using abstractions of infinite structures such as unbounded integers, infinite memory for allocation, unbounded space for call stack, unrestricted queue sizes and so on. It can be shown that for most classes of such systems, the verification problem is actually undecidable (there exists no algorithm which will always give the correct answer for arbitrary inputs). In spite of this negative theoretical result, techniques have been developed which are successful on some practical examples although they are not guaranteed to always work. This dissertation is in a similar spirit and develops a new paradigm for automated verification of large or infinite state systems. We observe that even if the state space of a system is infinite, for practical examples, the set of reachable states (or other fixpoints needed for verification) is often expressible in a simple representation. Based on this observation, we propose an entirely new approach to verification: the idea is to use techniques from computational learning theory to identify the reachable states (or other fixpoints) and then verify the property of interest. To use learning techniques, we solve key problems of either getting positive and negative examples for the fixpoint of interest or of answering membership and equivalence queries for this fixpoint. We show that learning-based verification is a powerful approach: as long as one has suitable algorithms which can learn the fixpoints needed and decision procedures for some common set-theoretic operations, one can guarantee that the verification procedure will either find a bug or prove that the system is correct. In particular, we have seen that for a large number of practical systems, the class of regular languages is rich enough to express these fixpoints, allowing us to automatically verify such systems using learning algorithms for regular sets. We show how the learning-based verification paradigm can be applied to a number of systems and for different kinds of specifications. First, we use learning to verify safety properties of finite state machines communicating over unbounded first-in-first-out channels. We assume that the reachable set of states is regular and use two different learning algorithms: one called RPNI which is based on learning from sample executions of the system, and the other derived from Angluin's L* algorithm which asks membership and equivalence queries. Next, we show how the learning approach can be used to verify safety properties of integer systems, parameterized systems and other systems in which states can be encoded as strings. We then extend the learning based approach to liveness properties and show how to use learning to verify omega-regular properties as well as CTL properties with fairness constraints. We have implemented the above techniques in a tool called LEVER. We analyze various examples using the tool and show how LEVER successfully verifies their properties. The running time is also comparable to other tools available. Moreover, since we can prove that our method will terminate whenever the target set that we are computing is regular, this is a substantial improvement over other tools which can guarantee completeness only under very specific conditions. We also present a detailed case study of a module in the Linux kernel called read-copy-update and successfully verify some interesting properties using our learning based method