Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KUHNRICH Morten SCHWOON Stefan KIEFER Stefan SRBA Jiří

Year of publication 2009
Type Article in Proceedings
Conference Proceedings of 12th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'09), pages 440-455, volume 5504 of LNCS, Springer-Verlag, 2009.
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-00596-1_31
Field Informatics
Keywords pushdown automata; semirings; verification
Description We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleenes 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 framework mentioned above and we describe a few applications to demonstrate its usability.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.