Reachability analysis of communicating pushdown systems

DOI10.1007/978-3-642-12032-9_19MaRDI QIDQ5900852zbMATH OpenOpenAlexFDO

Authors Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre

Publication date 27 April 2010

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve previous work from La Torre et al.

Recommendations

• Reachability analysis of communicating pushdown systems
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• Context-Bounded Analysis of Concurrent Queue Systems
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Reachability analysis of pushdown automata: Application to model-checking

Cited in

(22)

• Verifying parallel programs with dynamic communication structures
• Faster pushdown reachability analysis with applications in network verification
• Complexity results for reachability in cooperating systems and approximated reachability by abstract over-approximations
• Safety verification of asynchronous pushdown systems with shaped stacks
• Synchronizability for Verification of Asynchronously Communicating Systems
• Parameterised pushdown systems with non-atomic writes
• On bounded reachability analysis of shared memory systems
• On deciding synchronizability for asynchronously communicating systems
• Verifying communicating multi-pushdown systems via split-width
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• Verifying Parallel Programs with Dynamic Communication Structures
• scientific article; zbMATH DE number 7471708 (Why is no real title available?)
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
• Fully Dynamic Single-Source Reachability in Practice: An Experimental Study
• Analysis of message passing programs using SMT-solvers
• On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
• Context-Bounded Analysis of Concurrent Queue Systems
• Reachability analysis of communicating pushdown systems
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Parameterized verification under TSO with data types
• Weakly synchronous systems with three machines are Turing powerful
• Membership problems in finite groups

This page was built for publication: Reachability analysis of communicating pushdown systems

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