An axiomatic proof technique for parallel programs
From MaRDI portal
Publication:1219675
DOI10.1007/BF00268134zbMath0312.68011MaRDI QIDQ1219675
Publication date: 1976
Published in: Acta Informatica (Search for Journal in Brave)
Related Items
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, 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, Towards a Thread-Local Proof Technique for Starvation Freedom, A proof system for disjoint parallel quantum programs, Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency, Verifying a concurrent garbage collector with a rely-guarantee methodology, Joining specification statements, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, A weakest precondition semantics for communicating processes, A proof outline logic for object-oriented programming, Fair termination revisited - with delay, A proof technique for parallel programs, Cogent: uniqueness types and certifying compilation, Proof-based verification approaches for dynamic properties: application to the information system domain, Computation of equilibria in noncooperative games
Cites Work
- 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'
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
