Proofs of Networks of Processes
From MaRDI portal
Publication:3922150
DOI10.1109/TSE.1981.230844zbMath0468.68030MaRDI QIDQ3922150
Publication date: 1981
Published in: IEEE Transactions on Software Engineering (Search for Journal in Brave)
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items
A model and temporal proof system for networks of processes ⋮ Assume, Guarantee or Repair ⋮ Local Symmetry and Compositional Verification ⋮ Application of the composition principle to unity-like specifications ⋮ Applicability of fair simulation ⋮ Compositional Reasoning ⋮ Model Checking Parameterized Systems ⋮ Using logic to solve the submodule construction problem ⋮ Compositional System Security with Interface-Confined Adversaries ⋮ Modeling Actor Systems Using Dynamic I/O Automata ⋮ Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency ⋮ The Rely-Guarantee method for verifying shared variable concurrent programs ⋮ Theory and methodology of assumption/commitment based system interface specification and architectural contracts ⋮ Compositional semantics for real-time distributed computing ⋮ Automated circular assume-guarantee reasoning ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ Processes with infinite liveness requirements ⋮ Compositional analysis for linear systems ⋮ Towards a complete hierarchy of compositional dataflow models ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ Assumption/guarantee specifications in linear-time temporal logic (extended abstract) ⋮ A foundation for modular reasoning about safety and progress properties of state-based concurrent programs ⋮ An interface theory for service-oriented design ⋮ Automated program repair using formal verification techniques ⋮ The Birth of Model Checking ⋮ A proof technique for communicating sequential processes ⋮ A system for compositional verification of asynchronous objects ⋮ Equational reasoning about nondeterministic processes ⋮ Proof theory for exception handling in a tasking environment ⋮ Correctness of concurrent processes ⋮ Reasoning about programs by exploiting the environment ⋮ Assumption/guarantee specifications in linear-time temporal logic ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ A compositional axiomatization of statecharts ⋮ A class of systems with nearly zero distributed simulation overhead ⋮ Efficient distributed simulation of acyclic systems ⋮ A logical view of composition ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ A contract-based approach to adaptivity ⋮ Analysis of Executable Software Models ⋮ Compositional CSP Traces Refinement Checking ⋮ Assumption-Commitment Support for CSP Model Checking ⋮ Semantic models of a timed distributed dataspace architecture ⋮ Modular verification of multithreaded programs ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ Semantic specification and verification of data flow diagrams ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Axiomatic semantics of projection temporal logic programs ⋮ Automated Circular Assume-Guarantee Reasoning ⋮ Processes with local and global liveness requirements ⋮ P-A logic - a compositional proof system for distributed programs ⋮ ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS ⋮ Protocol Composition Logic (PCL) ⋮ Conditional Reactive Simulatability ⋮ The incompleteness of Misra and Chandy's proof systems ⋮ An explanatory presentation of composition rules for assumption- commitment specifications
