LEVER: A Tool for learning based verification
Software systems are often modeled using infinite structures such as
unbounded integers, infinite message queues and call stacks,
and unbounded number of processes. This makes
verification of these systems hard- in fact, for most common classes of
infinite state systems, the verification problem is
undecidable.
We have developed a new paradigm for verification of systems (possibly
infinite state) which is based on using techniques from computational
learning theory. Verification of systems usually entails computing either
the set of states reachable from the initial states or certain fixpoints
associated with logical formulas. To see our main idea, consider the problem of
identifying the set of reachable states which is needed for verifying safety
properties. Instead of computing this set by iteratively applying the
transition relation, we view it as a target set to be learned by answering
certain queries (such as membership and equivalence queries). In general,
these queries cannot be answered for the reachable states directly. To solve
this problem, instead of learning the reachable states, we learn a richer set of
state-witness pairs where a pair consists of a reachable state and a witness
which demonstrates how that state is reachable. We have shown that the
additional information in the witness allows both membership and equivalence
queries to be answered. Once the set of state-witness pairs is learned, the
reachable states are easily computed which can in turn be used to check the safety
property. We have also extended the learning technique to verify liveness
properties using either Computational Tree Logic with fairness or
omega-regular languages.
The learning based verification method enjoys several nice
properties. First, the running time of the verification algorithm
depends not on the time taken to converge to the fixpoint (which may not
even be achievable in a finite number of steps) but on the size of the
symbolic representation of the fixpoint. Second, it avoids the space
overhead of computing intermediate approximations to the
fixpoint. Finally, the learning
based verification method is sound (it never gives an incorrect
answer) and if the fixpoint set is representable in the symbolic
representation used by the learner, it is also complete (it is
guaranteed to terminate).
The LEVER tool can be downloaded here
The procedure for safety properties is shown below. CTL and omega regular properties are covered in Abhay Vardhan's PhD thesis.
