Faster algorithms for algebraic path properties in recursive state machines with constant treewidth

DOI10.1145/2676726.2676979MaRDI QIDQ2819794zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, Prateesh Goyal

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1410.7724

zbMATH Keywords

dataflow analysisinterprocedural analysisconstant treewidth graphsreachability and shortest path

Mathematics Subject Classification ID

Theory of programming languages (68N15) Formal languages and automata (68Q45) Graph theory (including graph drawing) in computer science (68R10)

Abstract: Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is emph{fixed} as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the emph{one-time} preprocessing vs for emph{each individual} query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks.

Recommendations

• Faster algorithms for weighted recursive state machines
• Algorithms for algebraic path properties in concurrent systems of constant treewidth components
• scientific article; zbMATH DE number 1796135
• Faster algorithms for quantitative verification in bounded treewidth graphs
• Subcubic algorithms for recursive state machines

Cited in

(8)

• What's decidable about program verification modulo axioms?
• Faster algorithms for weighted recursive state machines
• Tight bounds for reachability problems on one-counter and pushdown systems
• Efficient interprocedural data-flow analysis using treedepth and treewidth
• Graph Games and Reactive Synthesis
• Pushdown reachability with constant treewidth
• Faster algorithms for quantitative verification in bounded treewidth graphs
• Algorithms for algebraic path properties in concurrent systems of constant treewidth components

This page was built for publication: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819794)