Weighted pushdown systems and their application to interprocedural dataflow analysis

DOI10.1016/j.scico.2005.02.009zbMath1088.68040OpenAlexW4244831445MaRDI QIDQ2568453

David Melski, Somesh Jha, Stefan Schwoon, Thomas W. Reps

Publication date: 10 October 2005

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2005.02.009

zbMATH Keywords

generalized pushdown reachabilityinterprocedural dataflow analysismeet-over-all-paths problemweighted pushdown system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Automated enforcement for relaxed information release with reference points ⋮ Algebraic program analysis ⋮ Model Checking Procedural Programs ⋮ Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous ⋮ Summarization for termination: No return! ⋮ Winning Regions of Pushdown Parity Games: A Saturation Method ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Be lazy and don't care: faster CTL model checking for recursive state machines ⋮ Weighted iterated linear control ⋮ Convergence of Newton's method over commutative semirings ⋮ Sound Bit-Precise Numerical Domains ⋮ Solving Multiple Dataflow Queries Using WPDSs ⋮ Language Strength Reduction ⋮ Derivation Tree Analysis for Accelerated Fixed-Point Computation ⋮ Faster Algorithms for Weighted Recursive State Machines ⋮ Context-sensitive analysis without calling-context ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems ⋮ Derivation tree analysis for accelerated fixed-point computation ⋮ FPSOLVE: A Generic Solver for Fixpoint Equations Over Semirings ⋮ Weighted automata with storage ⋮ Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains ⋮ Interprocedural Analysis of Concurrent Programs Under a Context Bound ⋮ Program Analysis Using Weighted Pushdown Systems ⋮ A new abstraction framework for affine transformers ⋮ Reducing concurrent analysis under a context bound to sequential analysis ⋮ THE CHOMSKY-SCHÜTZENBERGER THEOREM FOR QUANTITATIVE CONTEXT-FREE LANGUAGES ⋮ Average Stack Cost of Büchi Pushdown Automata