Thread modularity at many levels: a pearl in compositional verification

DOI10.1145/3009837.3009893MaRDI QIDQ5370882zbMATH OpenOpenAlexFDO

Authors Jochen Hoenicke, Rupak Majumdar, Andreas Podelski

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

concurrencyparameterized verificationOwicki-Griesthread-modularity

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Proof spaces for unbounded parallelism
• scientific article; zbMATH DE number 3956417
• Precise Thread-Modular Verification
• scientific article; zbMATH DE number 1982207
• Modular verification of a non-blocking stack

Cited in

(7)

• RustHorn: CHC-based verification for Rust programs
• Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)
• Sound verification procedures for temporal properties of infinite-state systems
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• Temporal prophecy for proving temporal properties of infinite-state systems
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification

This page was built for publication: Thread modularity at many levels: a pearl in compositional verification

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