Verifying properties of parallel programs

DOI10.1145/360051.360224zbMath0322.68010OpenAlexW1965662337MaRDI QIDQ4085221

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)

Related Items

Convolution as a Unifying Concept, Verifying Visibility-Based Weak Consistency, On grainless footprint semantics for shared-memory programs, Automatic Inference of Access Permissions, Local Symmetry and Compositional Verification, A generalized deadlock predicate, Owicki-Gries Reasoning for Weak Memory Models, Compositional Reasoning, The formal development of a parallel program performing LU-decomposition, Syntactic Control of Interference and Concurrent Separation Logic, Deadlock-free absorption of barrier synchronisations, A perspective on specifying and verifying concurrent modules, A calculus and logic of resources and processes, Formal verification of concurrent programs with Read-write locks, Revisiting concurrent separation logic, Efficient algorithms for the maximum sum problems, A methodology for designing proof rules for fair parallel programs, A semantics for concurrent separation logic, Resources, concurrency, and local reasoning, A cylinder computation model for many-core parallel computing, Inter-process buffers in separation logic with rely-guarantee, Formal validation of data-parallel programs: a two-component assertional proof system for a simple language, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, The temporal semantics of concurrent programs, Verifying Switched System Stability With Logic, Transformational semantics for concurrent programs, The Birth of Model Checking, Synthesizing history and prophecy variables for symbolic model checking, Methods and means of parallel processing of information, Verification of object-oriented programs: a transformational approach, Verifying atomic data types, Parallel algorithms for the single source shortest path problem, Steps in modular specifications for concurrent modules (invited tutorial paper), A mechanical analysis of program verification strategies, Towards a foundation for semantics in complete metric spaces, Axiomatic system for proving the properties of simple multimodule programs, All-Path Reachability Logic, A Revisionist History of Concurrent Separation Logic, Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity, A brief history of process algebra, Unnamed Item, The pursuit of deadlock freedom, Fifty years of Hoare's logic, Corrigenda:Cooperating proofs for distributed programs with multiparty interactions, Fine-grained concurrency with separation logic, Current methods for proving program correctness, Local proofs for global safety properties, Distributed automata in an assumption-commitment framework, The lifeness property of on-the-fly garbage collector - a proof, An approach to automating the verification of compact parallel coordination programs. I, A proof technique for parallel programs