Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
From MaRDI portal
Publication:1187626
zbMath0674.68011MaRDI QIDQ1187626
Publication date: 23 January 1993
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
expressivenessconcurrencyproof systemssoundnessmodularityproof systemprocessmodular completenessadaptation completenesscompositional completenesscorrectness formulaefreeze predicatesHoare specificationsinvariant specificationsspecifying and verifying and reasoning about programs
Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Theory of operating systems (68N25) Theory of computing (68Q99)
Related Items
A compositional framework for fault tolerance by specification transformation ⋮ A trace-based compositional proof theory for fault tolerant distributed systems ⋮ A case study in transformational design of concurrent systems ⋮ Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency ⋮ Theory and methodology of assumption/commitment based system interface specification and architectural contracts ⋮ Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm ⋮ Refinement-Based Verification of Communicating Unstructured Code ⋮ Towards a complete hierarchy of compositional dataflow models ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ A foundation for modular reasoning about safety and progress properties of state-based concurrent programs ⋮ Synchronous development of asynchronous systems ⋮ A system for compositional verification of asynchronous objects ⋮ On the completeness of modular proof systems ⋮ Correctness of concurrent processes ⋮ On using temporal logic for refinement and compositional verification of concurrent systems ⋮ A compositional axiomatization of statecharts ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Interfaces between languages for communicating systems ⋮ Assumption-commitment support for CSP model checking
