Resource-constrained model checking of recursive programs.

*(English)*Zbl 1043.68524
Katoen, Joost-Pieter (ed.) et al., Tools and algorithms for the construction and analysis of systems. 8th international conference, TACAS 2002. Held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Berlin: Springer (ISBN 3-540-43419-4). Lect. Notes Comput. Sci. 2280, 236-250 (2002).

Summary: 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.

For the entire collection see [Zbl 0988.00082].

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.

For the entire collection see [Zbl 0988.00082].