Context-Bounded Analysis of Concurrent Queue Systems

DOI10.1007/978-3-540-78800-3_21zbMath1134.68446OpenAlexW1842117537MaRDI QIDQ5458334

Gennaro Parlato, P. Madhusudan, Salvatore La Torre

Publication date: 11 April 2008

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_21

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Realizability of concurrent recursive programs, Synchronizability for Verification of Asynchronously Communicating Systems, Parameterized Verification of Communicating Automata under Context Bounds, On deciding synchronizability for asynchronously communicating systems, The complexity of model checking multi-stack systems, Unnamed Item, Guessing the Buffer Bound for k-Synchronizability, Multiparty half-duplex systems and synchronous communications, On the \(k\)-synchronizability of systems, Verifying parallel programs with dynamic communication structures, Emptiness of Multi-pushdown Automata Is 2ETIME-Complete, Reachability of scope-bounded multistack pushdown systems, Unnamed Item, Unnamed Item, An Infinite Automaton Characterization of Double Exponential Time, On the Reachability Analysis of Acyclic Networks of Pushdown Systems, Temporal logics for concurrent recursive programs: satisfiability and model checking, A Sound Algorithm for Asynchronous Session Subtyping, The decidability of verification under PS 2.0, Data flow analysis of asynchronous systems using infinite abstract domains, Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete, Bounded Context Switching for Valence Systems, Verification of well-formed communicating recursive state machines, On the path-width of integer linear programming, Games on Multi-stack Pushdown Systems, Deciding branching time properties for asynchronous programs, Realizability of Concurrent Recursive Programs, Unnamed Item, Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations, Non axiomatisability of positive relation algebras with constants, via graph homomorphisms, Unnamed Item, Games on Higher Order Multi-stack Pushdown Systems, Generalized Post embedding problems, Guessing the buffer bound for k-synchronizability

Cites Work

• Unnamed Item
• Complexity results for 1-safe nets
• Analysis of a class of communicating finite state machines
• Verification in loosely synchronous queue-connected discrete timed automata.
• VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES
• Interprocedural analysis of asynchronous programs
• Decidability Results for Well-Structured Transition Systems with Auxiliary Storage
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science