Verification of parameterized concurrent programs by modular reasoning about data and control

DOI10.1145/2103656.2103693MaRDI QIDQ2942881zbMATH OpenOpenAlexFDO

Authors Azadeh Farzan, Zachary Kincaid

Publication date 11 September 2015

Published in Proceedings of the 39th 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/2103656.2103693

zbMATH Keywords

abstract interpretationcompositional reasoningconcurrencydata flow graphsparameterized programsthread invariants

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)

Recommendations

• Modular verification for shared-variable concurrent programs
• Modular verification of concurrent programs via sequential model checking
• A perspective on specifying and verifying concurrent modules
• Specification and verification of concurrent programs through refinements
• Modular verification of concurrency-aware linearizability
• Verification of fine-grain concurrent programs
• Verification of concurrent programs: The automata-theoretic framework
• Modular verification of multithreaded programs

Cited in

(11)

• A tree-based approach to data flow proofs
• Verification of concurrent programs using Petri net unfoldings
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Compositional reasoning
• PBMC: Symbolic Slicing for the Verification of Concurrent Programs
• Abstract threads
• Parametrized invariance for infinite state processes
• Verification by Parallelization of Parametric Code
• Clustered relational thread-modular abstract interpretation with local traces
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Lost in abstraction: monotonicity in multi-threaded programs

This page was built for publication: Verification of parameterized concurrent programs by modular reasoning about data and control

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