Compositionality Entails Sequentializability

DOI10.1007/978-3-642-19835-9_4MaRDI QIDQ3000634zbMATH OpenOpenAlexFDO

Authors Pranav Garg, Parthasarathy Madhusudan

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19835-9_4

zbMATH Keywords

compositional verificationconcurrent programssequentialization

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Compositional properties of sequential processes
• Sequentiality in an extensional framework
• scientific article; zbMATH DE number 431761
• Revisiting sequential composition in process calculi
• Composing ordered sequential consistency
• scientific article; zbMATH DE number 1638658
• On sequential separability
• Denotational linear time semantics and sequential composition
• Sequential composition in the presence of intermediate termination (extended abstract)
• scientific article; zbMATH DE number 7471704

Cites work

• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• An approach to automating the verification of compact parallel coordination programs. I
• An axiomatic proof technique for parallel programs
• Computer Aided Verification
• Local Proofs for Global Safety Properties
• Local rely-guarantee reasoning
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Tentative steps toward a development method for interfering programs
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(10)

• Compositional sequentialization of periodic programs
• Modular verification of concurrent programs via sequential model checking
• Layered concurrent programs
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• scientific article; zbMATH DE number 1612485 (Why is no real title available?)
• Sequentialization using timestamps
• Compositional reasoning
• scientific article; zbMATH DE number 3956417 (Why is no real title available?)
• On reduction of sequential-parallel compositional programs to entirely sequential form
• Composing ordered sequential consistency

Describes a project that uses

Uses Software

• Boogie
• SLAM

This page was built for publication: Compositionality Entails Sequentializability

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