Safety verification of asynchronous pushdown systems with shaped stacks

DOI10.1007/978-3-642-40184-8_21MaRDI QIDQ2842115zbMATH OpenOpenAlexFDO

Authors Jonathan Kochems, C.-H. Luke Ong

Publication date 12 August 2013

Published in CONCUR 2013 – Concurrency Theory (Search for Journal in Brave)

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

zbMATH Keywords

asynchronous message passingpushdown systemsverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: In this paper, we study the program-point reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers. Our goal is to relax the common restriction that messages can only be retrieved by a pushdown process when its stack is empty. We use the notion of partially commutative context-free grammars to describe a new class of asynchronously communicating pushdown systems with a mild shape constraint on the stacks for which the program-point coverability problem remains decidable. Stacks that fit the shape constraint may reach arbitrary heights; further a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. This class extends previous computational models studied in the context of asynchronous programs, and enables the safety verification of a large class of message passing programs.

Recommendations

• Reachability analysis of communicating pushdown systems
• scientific article; zbMATH DE number 6831517
• Reachability analysis of communicating pushdown systems
• Reachability of scope-bounded multistack pushdown systems
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems

Cited in

(3)

• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Data flow analysis of asynchronous systems using infinite abstract domains
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable

This page was built for publication: Safety verification of asynchronous pushdown systems with shaped stacks

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