Complexity of pattern-based verification for multithreaded programs

DOI10.1145/1926385.1926443MaRDI QIDQ5408569zbMATH OpenOpenAlexWikidataFDO

Authors Javier Esparza, Pierre Ganty

Publication date 10 April 2014

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

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

zbMATH Keywords

concurrent programmingcontext-free languagessafety

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Causality-based verification of multi-threaded programs
• Constraint-based automatic verification of abstract models of multithreaded programs
• Abstract threads
• Thread-Modular Verification Is Cartesian Abstract Interpretation

Cited in

(16)

• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Parikh's theorem: a simple and direct automaton construction
• Generalised multi-pattern-based verification of programs with linear linked structures
• A complete refinement procedure for regular separability of context-free languages
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Causality-based verification of multi-threaded programs
• Interprocedural reachability for flat integer programs
• Constraint-based automatic verification of abstract models of multithreaded programs
• Checking a Multithreaded Algorithm with  + CAL
• Bounded underapproximations
• Unboundedness problems for languages of vector addition systems
• On the Complexity of Bounded Context Switching.
• Verifying multithreaded recursive programs with integer variables
• Parametric runtime verification is NP-complete and coNP-complete
• Reasoning about reversal-bounded counter machines
• An introduction to the theory of linear integer arithmetic (invited paper)

This page was built for publication: Complexity of pattern-based verification for multithreaded programs

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