Verifying properties of parallel programs

DOI10.1145/360051.360224MaRDI QIDQ4085221zbMATH OpenOpenAlexFDO

Authors Susan Owicki, David Gries

Publication date 1976

Published in Communications of the ACM (Search for Journal in Brave)

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

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Algorithms in computer science (68W99)

Cited in

(53)

• Local proofs for global safety properties
• The lifeness property of on-the-fly garbage collector - a proof
• An approach to automating the verification of compact parallel coordination programs. I
• A generalized deadlock predicate
• The formal development of a parallel program performing LU-decomposition
• Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
• The temporal semantics of concurrent programs
• Transformational semantics for concurrent programs
• Methods and means of parallel processing of information
• Parallel algorithms for the single source shortest path problem
• Towards a foundation for semantics in complete metric spaces
• Deadlock-free absorption of barrier synchronisations
• A methodology for designing proof rules for fair parallel programs
• Formal validation of data-parallel programs: a two-component assertional proof system for a simple language
• A perspective on specifying and verifying concurrent modules
• Efficient algorithms for the maximum sum problems
• A brief history of process algebra
• Corrigenda:Cooperating proofs for distributed programs with multiparty interactions
• Distributed automata in an assumption-commitment framework
• Fifty years of Hoare's logic
• Revisiting concurrent separation logic
• On grainless footprint semantics for shared-memory programs
• Automatic inference of access permissions
• Local symmetry and compositional verification
• Compositional reasoning
• Syntactic control of interference and concurrent separation logic
• Owicki-Gries reasoning for weak memory models
• The Birth of Model Checking
• Formal verification of concurrent programs with Read-write locks
• Axiomatic system for proving the properties of simple multimodule programs
• Current methods for proving program correctness
• A cylinder computation model for many-core parallel computing
• Verification of object-oriented programs: a transformational approach
• Verifying visibility-based weak consistency
• Order out of chaos: proving linearizability using local views
• Convolution as a Unifying Concept
• A revisionist history of concurrent separation logic
• The pursuit of deadlock freedom
• Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Verifying Switched System Stability With Logic
• Inter-process buffers in separation logic with rely-guarantee
• Synthesizing history and prophecy variables for symbolic model checking
• Choose your proofs: commutativity and symmetry for smarter reasoning
• The autonomous data language -- concepts, design and formal verification
• Tony Hoare: his path to the ACM Turing Award
• Fine-grained concurrency with separation logic
• A proof technique for parallel programs
• A calculus and logic of resources and processes
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Verifying atomic data types
• A mechanical analysis of program verification strategies

This page was built for publication: Verifying properties of parallel programs

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