Interprocedural reachability for flat integer programs

DOI10.1007/978-3-319-22177-9_11MaRDI QIDQ2947875zbMATH OpenOpenAlexFDO

Authors Pierre Ganty, Radu Iosif

Publication date 29 September 2015

Published in Fundamentals of Computation Theory (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Abstract: We study programs with integer data, procedure calls and arbitrary call graphs. We show that, whenever the guards and updates are given by octagonal relations, the reachability problem along control flow paths within some language w1* ... wd* over program statements is decidable in Nexptime. To achieve this upper bound, we combine a program transformation into the same class of programs but without procedures, with an Np-completeness result for the reachability problem of procedure-less programs. Besides the program, the expression w1* ... wd* is also mapped onto an expression of a similar form but this time over the transformed program statements. Several arguments involving context-free grammars and their generative process enable us to give tight bounds on the size of the resulting expression. The currently existing gap between Np-hard and Nexptime can be closed to Np-complete when a certain parameter of the analysis is assumed to be constant.

Recommendations

• Reachability Analysis of Procedural Programs with Affine Integer Arithmetic
• Safety problems are NP-complete for flat integer programs with octagonal loops
• Decision procedures for flat array properties
• Iterating Octagons
• scientific article; zbMATH DE number 1407672

Cites work

• scientific article; zbMATH DE number 3293666 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• A family of languages having only finite-index grammars
• Accelerating interpolants
• Adding nesting structure to words
• Approximating Petri net reachability along context-free traces
• Complexity of pattern-based verification for multithreaded programs
• Control sets on grammars using depth-first derivations
• Fast acceleration of ultimately periodic relations
• Invariant Checking for Programs with Procedure Calls
• Push-down automata with gap-order constraints
• Safety problems are NP-complete for flat integer programs with octagonal loops
• Taming past LTL and flat counter systems
• The octagon abstract domain
• Underapproximation of procedure summaries for integer programs
• Verification of gap-order constraint abstractions of counter systems

Cited in

(4)

• Safety problems are NP-complete for flat integer programs with octagonal loops
• Automatic verification of recursive procedures with one integer parameter.
• Forward analysis and model checking for trace bounded WSTS
• Reachability Analysis of Procedural Programs with Affine Integer Arithmetic

This page was built for publication: Interprocedural reachability for flat integer programs

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