2014/10/28 by Krishnendu Chatterjee, Chatterjee, Krishnendu, Rasmus Ibsen-Jensen +5
Computer Science · #Advanced Database Systems and Queries #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1410.7724
openalex publication_date 2014/10/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Interprocedural analysis is at the heart of numerous applications in\nprogramming languages, such as alias analysis, constant propagation, etc.\nRecursive state machines (RSMs) are standard models for interprocedural\nanalysis. We consider a general framework with RSMs where the transitions are\nlabeled from a semiring, and path properties are algebraic with semiring\noperations. RSMs with algebraic path properties can model interprocedural\ndataflow analysis problems, the shortest path problem, the most probable path\nproblem, etc. The traditional algorithms for interprocedural analysis focus on\npath properties where the starting point is \fixed as the entry point of\na specific method. In this work, we consider possible multiple queries as\nrequired in many applications such as in alias analysis. The study of multiple\nqueries allows us to bring in a very important algorithmic distinction between\nthe resource usage of the \one-time preprocessing vs for \each\nindividual query. The second aspect that we consider is that the control flow\ngraphs for most programs have constant treewidth.\n Our main contributions are simple and implementable algorithms that support\nmultiple queries for algebraic path properties for RSMs that have constant\ntreewidth. Our theoretical results show that our algorithms have small\nadditional one-time preprocessing, but can answer subsequent queries\nsignificantly faster as compared to the current best-known solutions for\nseveral important problems, such as interprocedural reachability and shortest\npath. We provide a prototype implementation for interprocedural reachability\nand intraprocedural shortest path that gives a significant speed-up on several\nbenchmarks.\n