Realizability of Concurrent Recursive Programs

DOI10.1007/978-3-642-00596-1_29MaRDI QIDQ3617744zbMATH OpenOpenAlexFDO

Authors Benedikt Bollig, Manuela-Lidia Grindei, Peter Habermehl

Publication date 31 March 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-00596-1_29

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Realizability of concurrent recursive programs
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
• Verification of concurrent programs: The automata-theoretic framework
• The complexity of model checking multi-stack systems

Cites work

• A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
• A Kleene theorem and model checking algorithms for existentially bounded communicating automata
• A theory of regular MSC languages
• Adding Nesting Structure to Words
• An algorithmic approach for checking closure properties of temporal logic specifications and -regular languages
• Constructing Exponential-Size Deterministic Zielonka Automata
• Context-Bounded Analysis of Concurrent Queue Systems
• First-Order and Temporal Logics for Nested Words
• scientific article; zbMATH DE number 1305002 (Why is no real title available?)
• scientific article; zbMATH DE number 1500652 (Why is no real title available?)
• scientific article; zbMATH DE number 1418329 (Why is no real title available?)
• LTL is expressively complete for Mazurkiewicz traces
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Notes on finite asynchronous automata
• On the Expressive Power of 2-Stack Visibly Pushdown Automata
• Synthesis of distributed algorithms using asynchronous automata.
• Tools and Algorithms for the Construction and Analysis of Systems
• Unfolding Synthesis of Asynchronous Automata
• Using branching time temporal logic to synthesize synchronization skeletons
• Visibly pushdown languages
• Weighted asynchronous cellular automata

Cited in

(10)

• Realizability of concurrent recursive programs
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Real-time properties of indirect recursive procedures
• Verification of concurrent programs: The automata-theoretic framework
• On Distributed Monitoring and Synthesis
• Automated synthesis of distributed controllers
• The language theory of bounded context-switching
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• A survey on automata with translucent letters
• Step semantics for ``true concurrency with recursion

This page was built for publication: Realizability of Concurrent Recursive Programs

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