Resource-constrained model checking of recursive programs

A number of recent papers present efficient algorithms for LTL model checking for recursive programs with finite data structures. A common feature in all these works is that they consider infinitely long runs of the program without regard to the size of the program stack. Runs requiring unbounded stack are often a result of abstractions done to obtain a finite-data recursive program. In this paper, we introduce the notion of resource-constrained model checking where we distinguish between stack-diverging runs and finite-stack runs. It should be noted that finiteness of stack-like resources cannot be expressed in LTL. We develop resource-constrained model checking in terms of good cycle detection in a finite graph called R-graph, which is constructed from a given push-down system (PDS) and a Büchi automaton. We make the formulation of the model checker "executable" by encoding it directly as Horn clauses. We present a local algorithm to detect a good cycle in an R-graph. Furthermore, by describing the construction of R-graph as a logic program and evaluating it using tabled resolution, we do model checking without materializing the push-down system or the induced R-graph. Preliminary experiments indicate that the local model checker is at least as efficient as existing model checkers for push-down systems.