A generic approach to the static analysis of concurrent programs with procedures

DOI10.1145/604131.604137MaRDI QIDQ2942913zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Javier Esparza, Tayssir Touili

Publication date 11 September 2015

Published in Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/604131.604137

zbMATH Keywords

abstractionconcurrent programs with proceduresKleene algebraspushdown systemsstatic analysisverification

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45)

Recommendations

• A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Reachability analysis of synchronized PA systems
• scientific article; zbMATH DE number 1948384
• Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous

Cites work

• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 615137 (Why is no real title available?)
• scientific article; zbMATH DE number 1942450 (Why is no real title available?)
• scientific article; zbMATH DE number 1948151 (Why is no real title available?)
• scientific article; zbMATH DE number 1953123 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• Regular expression pattern matching for XML
• Types and programing languages

Cited in

(30)

• Verifying parallel programs with dynamic communication structures
• Model checking dynamic pushdown networks
• On the sequential nature of interprocedural program-analysis problems
• A complete refinement procedure for regular separability of context-free languages
• scientific article; zbMATH DE number 1670564 (Why is no real title available?)
• An abstract analysis framework for synchronous concurrent languages based on source-to-source transformation
• Static analysis of communicating processes using symbolic transducers
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Reasoning about threads with bounded lock chains
• Model checking concurrent programs
• Invariant Checking for Programs with Procedure Calls
• Static Analysis of Concurrent Programs Using Ordinary Differential Equations
• Solving Multiple Dataflow Queries Using WPDSs
• Language Strength Reduction
• Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
• Verifying Parallel Programs with Dynamic Communication Structures
• scientific article; zbMATH DE number 1948384 (Why is no real title available?)
• Bounded underapproximations
• Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous
• Bounded communication reachability analysis of process rewrite systems with ordered parallelism
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Program Analysis Using Weighted Pushdown Systems
• Derivation tree analysis for accelerated fixed-point computation
• A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
• Verification, Model Checking, and Abstract Interpretation
• Reachability analysis of pushdown systems with an upper stack
• Backwards-reachability for cooperating multi-pushdown systems
• A consistency analysis of a class of concurrent transient implicit/explicit algorithms
• Compositional verification of sequential programs with procedures
• Verification of well-formed communicating recursive state machines

Describes a project that uses

Uses Software

• TREX

This page was built for publication: A generic approach to the static analysis of concurrent programs with procedures

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