Tentative steps toward a development method for interfering programs
From MaRDI portal
Publication:3666252
DOI10.1145/69575.69577zbMath0517.68032OpenAlexW2090551028MaRDI QIDQ3666252
No author found.
Publication date: 1983
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/69575.69577
verificationcommunicating sequential processesspecification methodguarantee- conditionsrely-conditions
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items
Regression Verification for Multi-threaded Programs, Local Symmetry and Compositional Verification, Application of the composition principle to unity-like specifications, Certifying low-level programs with hardware interrupts and preemptive threads, Compositional Reasoning, Compositional System Security with Interface-Confined Adversaries, Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency, Generalised rely-guarantee concurrency: an algebraic foundation, Formal verification of concurrent programs with Read-write locks, Certifying assembly programs with trails, An application of temporal projection to interleaving concurrency, Splitting atoms safely, A Program Construction and Verification Tool for Separation Logic, Compositional probabilistic verification through multi-objective model checking, A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, Assumption/guarantee specifications in linear-time temporal logic (extended abstract), Designing a semantic model for a wide-spectrum language with concurrency, Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example, Balancing expressiveness in formal approaches to concurrency, Verifying a concurrent garbage collector using a rely-guarantee methodology, A fine-grained semantics for arrays and pointers under weak memory models, Unnamed Item, Counterexample-guided abstraction refinement for symmetric concurrent programs, Compositional verification of a communication protocol for a remotely operated aircraft, The Composition of Event-B Models, Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Interconnections between classes of sequentially compositional temporal formulas, Verification of evolving software via component substitutability analysis, Compositionality Entails Sequentializability, Assumption/guarantee specifications in linear-time temporal logic, Verifying correctness of persistent concurrent data structures: a sound and complete method, Conditions of contracts for separating responsibilities in heterogeneous systems, A compositional protocol verification using relativized bisimulation, A compositional axiomatization of statecharts, Guest editors' preface to special issue on interval temporal logics, Compositional reasoning using intervals and time reversal, Transfer Principles for Reasoning About Concurrent Programs, Proving linearizability with temporal logic, Elucidating concurrent algorithms via layers of abstraction and reification, Semantic models of a timed distributed dataspace architecture, Modular verification of multithreaded programs, Encoding fairness in a synchronous concurrent program algebra, A wide-spectrum language for verification of programs on weak memory models, Compositional reasoning for shared-variable concurrent programs, Compositional analysis of C/C++ programs with veriSoft, An introduction to compositional methods for concurrency and their application to real-time., Fifty years of Hoare's logic, Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation), An operational semantics for object-oriented concepts based on the class hierarchy, Reasoning about goal-directed real-time teleo-reactive programs, Derivation of concurrent programs by stepwise scheduling of Event-B models, Verifying a concurrent garbage collector with a rely-guarantee methodology, Composing leads-to properties, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, A verification-driven framework for iterative design of controllers, ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS, Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach, Protocol combinators for modeling, testing, and execution of distributed systems, Reasoning about Separation Using Abstraction and Reification, An explanatory presentation of composition rules for assumption- commitment specifications
