Interprocedural Reachability for Flat Integer Programs

DOI10.1007/978-3-319-22177-9_11zbMath1434.68107arXiv1405.3069MaRDI QIDQ2947875

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

68Q25: Analysis of algorithms and problem complexity

68Q42: Grammars and rewriting systems

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Forward analysis and model checking for trace bounded WSTS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• The octagon abstract domain
• Verification of gap-order constraint abstractions of counter systems
• Taming Past LTL and Flat Counter Systems
• Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
• Nonelementary Complexities for Branching VASS, MELL, and Extensions
• Push-Down Automata with Gap-Order Constraints
• Invariant Checking for Programs with Procedure Calls
• Adding nesting structure to words
• Fast Acceleration of Ultimately Periodic Relations
• A family of languages having only finite-index grammars
• Control sets on grammars using depth-first derivations
• Accelerating Interpolants
• Underapproximation of Procedure Summaries for Integer Programs
• Complexity of pattern-based verification for multithreaded programs