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

DOI10.1145/604131.604137zbMath1321.68185OpenAlexW2160520283MaRDI QIDQ2942913

Ahmed Bouajjani, Tayssir Touili, Javier Esparza

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

verificationstatic analysisabstractionpushdown systemsKleene algebrasconcurrent programs with procedures

Mathematics Subject Classification ID

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

Related Items (18)

A complete refinement procedure for regular separability of context-free languages ⋮ Model Checking Concurrent Programs ⋮ Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous ⋮ Solving Multiple Dataflow Queries Using WPDSs ⋮ Language Strength Reduction ⋮ Bounded underapproximations ⋮ Verifying parallel programs with dynamic communication structures ⋮ Compositional verification of sequential programs with procedures ⋮ Verification of well-formed communicating recursive state machines ⋮ Reachability Analysis of Pushdown Systems with an Upper Stack ⋮ Derivation tree analysis for accelerated fixed-point computation ⋮ 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 ⋮ Reasoning about Threads with Bounded Lock Chains ⋮ Verifying Parallel Programs with Dynamic Communication Structures ⋮ Invariant Checking for Programs with Procedure Calls ⋮ Model checking dynamic pushdown networks

Uses Software

• TREX

Cites Work

• Regular expression pattern matching for XML
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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