An axiomatic proof technique for parallel programs

DOI10.1007/BF00268134zbMath0312.68011MaRDI QIDQ1219675

David Gries, Susan Owicki

Publication date: 1976

Published in: Acta Informatica (Search for Journal in Brave)

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items (only showing first 100 items - show all)

A Hoare Logic for GPU Kernels ⋮ Weighted synchronous automata ⋮ Parallelized sequential composition and hardware weak memory models ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Modular verification for shared-variable concurrent programs ⋮ Reasoning about promises in weak memory models with event structures ⋮ Loop invariants ⋮ A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs ⋮ Reasoning about Recursive Processes in Shared-Variable Concurrency ⋮ A Proof System for a PGAS Language ⋮ Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation) ⋮ Relation-based semantics for concurrency ⋮ Process algebra with guards: Combining hoare logic with process algebra ⋮ An implementation of mutual inclusion ⋮ Regression Verification for Multi-threaded Programs ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Automatic workflow verification and generation ⋮ Bounded model checking of infinite state systems ⋮ Invariants for the construction of a handshake register ⋮ Owicki-Gries Reasoning for Weak Memory Models ⋮ A principle for sequential reasoning about distributed algorithms ⋮ Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ The formal development of a parallel program performing LU-decomposition ⋮ Invariants, composition, and substitution ⋮ Compositional verification of smart contracts through communication abstraction ⋮ On the programs-as-formulas interpretation of parallel programs in Peano arithmetic ⋮ Bounded delay for a free address ⋮ Fairness and the axioms of control predicates ⋮ Global renaming operators in concrete process algebra ⋮ A generalization of Owicki-Gries's Hoare logic for a concurrent while language ⋮ The Rely-Guarantee method for verifying shared variable concurrent programs ⋮ Theory and methodology of assumption/commitment based system interface specification and architectural contracts ⋮ Atomic semantics of nonatomic programs ⋮ Splitting atoms safely ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ The use of hoare logic in the verification of horizontal microprograms ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ Tournaments for mutual exclusion: verification and concurrent complexity ⋮ A proof system for asynchronously communicating deterministic processes ⋮ A coinductive calculus for asynchronous side-effecting processes ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Semantics of nondeterminism, concurrency, and communication ⋮ The temporal semantics of concurrent programs ⋮ Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS ⋮ Local optimization of colorings of graphs ⋮ Arithmetical completeness in first-order dynamic logic for concurrent programs ⋮ A system for compositional verification of asynchronous objects ⋮ Verification of object-oriented programs: a transformational approach ⋮ Interpreting one concurrent calculus in another ⋮ Compositional verification of a communication protocol for a remotely operated aircraft ⋮ Proof theory for exception handling in a tasking environment ⋮ A mechanized refinement proof of the Chase-Lev deque using a proof system ⋮ Proving Linearizability Using Partial Orders ⋮ Starvation-free mutual exclusion with semaphores ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ Towards formally specifying and verifying transactional memory ⋮ Wait-free linearization with an assertional proof ⋮ Wait-free linearization with a mechanical proof ⋮ Fast timing-based algorithms ⋮ Automatic verification for a class of distributed systems ⋮ Wait-free concurrent memory management by Create and Read until Deletion (CaRuD) ⋮ A proof system for adaptable class hierarchies ⋮ Reasoning about programs by exploiting the environment ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ Compositionality Entails Sequentializability ⋮ CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs ⋮ Formal derivation of an algorithm for distributed phase synchronization ⋮ On using temporal logic for refinement and compositional verification of concurrent systems ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) ⋮ A compositional protocol verification using relativized bisimulation ⋮ Defining conditional independence using collapses ⋮ A class of systems with nearly zero distributed simulation overhead ⋮ Logical foundations for programming semantics ⋮ Using Hoare Logic in a Process Algebra Setting ⋮ Queue based mutual exclusion with linearly bounded overtaking ⋮ Hybrid process algebra ⋮ Verification of Concurrent Systems with VerCors ⋮ Incremental reasoning with lazy behavioral subtyping for multiple inheritance ⋮ An assertion-based proof system for multithreaded Java ⋮ A unified approach of program verification ⋮ Lazy behavioral subtyping ⋮ Synchronous Kleene algebra ⋮ Auxiliary variables in partial correctness programming logics ⋮ Incremental Reasoning for Multiple Inheritance ⋮ Fifty years of Hoare's logic ⋮ Axiomatic semantics of projection temporal logic programs ⋮ A shared-variable concurrency analysis of multi-threaded object-oriented programs ⋮ Correctness and concurrent complexity of the black-white bakery algorithm ⋮ Verifying traits: an incremental proof system for fine-grained reuse ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ A starvation-free solution to the mutual exclusion problem

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving properties of interacting processes
• Correctness of parallel programs: The Church-Rosser approach
• Consistent and complementary formal theories of the semantics of programming languages
• The structure of the “THE”-multiprogramming system
• An axiomatic basis for computer programming
• Proof of a structured program: 'The sieve of Eratosthenes'

This page was built for publication: An axiomatic proof technique for parallel programs