Verifying parallel programs with dynamic communication structures

DOI10.1016/J.TCS.2010.05.028MaRDI QIDQ1959654zbMATH OpenOpenAlexFDO

Authors Tayssir Touili, Mohamed Faouzi Atig

Publication date 7 October 2010

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2010.05.028

zbMATH Keywords

model checkingreachability analysisrecognizable setsconcurrent programspushdown networks

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Verifying Parallel Programs with Dynamic Communication Structures
• scientific article; zbMATH DE number 3890706
• A survey of verification techniques for parallel programs
• Automatic verification of determinism for structured parallel programs
• scientific article; zbMATH DE number 4119602
• On verification of parallel message-passing processes
• Verifying the correctness of distributed systems via mergeable parallelism
• Dynamic symbolic verification of MPI programs

Cites work

• scientific article; zbMATH DE number 1232241 (Why is no real title available?)
• scientific article; zbMATH DE number 1304991 (Why is no real title available?)
• scientific article; zbMATH DE number 1538033 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 2090847 (Why is no real title available?)
• A generic approach to the static analysis of concurrent programs with procedures
• CONCUR 2005 – Concurrency Theory
• Computer Aided Verification
• Context-Bounded Analysis of Concurrent Queue Systems
• Decidability Results for Well-Structured Transition Systems with Auxiliary Storage
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• On the analysis of interacting pushdown systems
• Reachability analysis of communicating pushdown systems
• Reachability analysis of pushdown automata: Application to model-checking
• Term Rewriting and Applications
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

• Model checking dynamic pushdown networks
• Model checking concurrent programs
• Verifying Parallel Programs with Dynamic Communication Structures
• Refinement-Based Verification of Communicating Unstructured Code
• Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
• Verification of programs with half-duplex communication
• Tools and Algorithms for the Construction and Analysis of Systems
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types

Describes a project that uses

Uses Software

• MAGIC

This page was built for publication: Verifying parallel programs with dynamic communication structures

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