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

context-free languagesconcurrent programmingsafety

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

(15)

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

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)