Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Analysing Mu-Calculus Properties of Pushdown Systems
verfasst von : Matthew Hague, C. -H. Luke Ong
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Pushdown systems provide a natural model of software with recursive procedure calls. We provide a tool (PDSolver) implementing an algorithm for computing the winning regions of a pushdown parity game and its adaptation to the direct computation of modal
μ
-calculus properties over pushdown systems. We also extend the algorithm to allow backwards, as well as forwards, modalities and allow the user to restrict the control flow graph to configurations reachable from a designated initial state. These extensions are motivated by applications in dataflow analysis. We provide two sets of experimental data. First, we obtain a picture of the general behaviour by analysing random problem instances. Secondly, we use the tool to perform dataflow analysis on real-world Java programs, taken from the DaCapo benchmark suite.