Academic
Publications
Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains

Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains,10.1007/978-3-642-00596-1_31,Computing Research Repository,Morte

Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains   (Citations: 2)
BibTex | RIS | RefWorks Download
We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the frame- work mentioned above and we describe a few applications to demonstrate its usability.
Journal: Computing Research Repository - CORR , vol. abs/0901.0, pp. 440-455, 2009
Cumulative Annual
    • ...Additionally in recent work [12,13], new techniques have been presented to solve equations for more general types of semirings...

    Alexander Wenner. Weighted Dynamic Pushdown Networks

    • ...A full version of the paper is available as [12]...
    • ...Our contribution is that we prove that it works also for polynomials of higher degrees where more involved technical treatment is necessary. Details are presented in [12]...
    • ...treatment only for the predecessors; the computation of successors is analogous and it is provided in [12]...
    • ...A similar conclusion about the complexity of the algorithm for computing successors can be drawn thanks to the (linear) connection between forward and backward reachability analysis described in [12]...
    • ...The problem of computing successors is also considered in [20], i.e., computing a W-automaton A where vA(c) is the meet-over-all-paths from an initial configuration c0 to c. Using our technique, this result can also be extended to unbounded semirings; [12] shows an equation system for this problem, which can be converted into a W-automaton for post ∗(c0) in analogous fashion...
    • ...As mentioned in Section 3, this automaton can be normalized in linear time and we can then build a weighted post ∗({pX}) W-automaton, of size O(n2) with O(n) states and in time O(n4). Details can be found in [12]...

    Morten Kühnrichet al. Interprocedural Dataflow Analysis over Weight Domains with Infinite De...

Sort by: