Analysis of Recursive Game Graphs Using Data Flow Equations

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Given a finite-state abstraction of a sequential program with potentially recursive procedures and input from the environment, we wish to check statically whether there are input sequences that can drive the system into “bad/good” executions. Pushdown games have been used in recent years for such analyses and there is by now a very rich literature on the subject. (See, e.g., [BS92,Tho95,Wal96,BEM97,Cac02a,CDT02].)

In this paper we use recursive game graphs to model such interprocedural control flow in an open system. These models are intimately related to pushdown systems and pushdown games , but more directly capture the control flow graphs of recursive programs ([AEY01,BGR01,ATM03b]).

We describe alternative algorithms for the well-studied problems of determining both reachability and Büchi winning strategies in such games. Our algorithms are based on solutions to second-order data flow equations, generalizing the Datalog rules used in [AEY01] for analysis of recursive state machines. This offers what we feel is a conceptually simpler view of these well-studied problems and provides another example of the close links between the techniques used in program analysis and those of model checking.

There are also some technical advantages to the equational approach. Like the approach of Cachat [Cac02a], our solution avoids the necessarily exponential-space blow-up incurred by Walukiewicz’s algorithms for pushdown games. However, unlike [Cac02a], our approach does not rely on a representation of the space of winning configurations of a pushdown graph by (alternating) automata. Only “minimal” sets of exits that can be “forced” need to be maintained, and this provides the potential for greater space efficiency. In a sense, our algorithms can be viewed as an “automaton-free” version of the algorithms of [Cac02a].
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings
PublisherSpringer Berlin Heidelberg
Pages282-296
Number of pages15
Volume2937
ISBN (Electronic)978-3-540-24622-0
ISBN (Print)978-3-540-20803-7
DOIs
Publication statusPublished - 2004

Fingerprint

Dive into the research topics of 'Analysis of Recursive Game Graphs Using Data Flow Equations'. Together they form a unique fingerprint.

Cite this