Tentative steps toward a development method for interfering programs

DOI10.1145/69575.69577zbMATH Open0517.68032OpenAlexW2090551028MaRDI QIDQ3666252FDOQ3666252

Author name not available (Why is that?)

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

zbMATH Keywords

verificationcommunicating sequential processesspecification methodguarantee- conditionsrely-conditions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Cited In (67)

• Extending rely-guarantee thinking to handle real-time scheduling
• AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
• Protocol combinators for modeling, testing, and execution of distributed systems
• Asynchronous Cooperative Contracts for Cooperative Scheduling
• Compositional System Security with Interface-Confined Adversaries
• A fine-grained semantics for arrays and pointers under weak memory models
• Transfer Principles for Reasoning About Concurrent Programs
• An introduction to compositional methods for concurrency and their application to real-time.
• A parametric rely-guarantee reasoning framework for concurrent reactive systems
• Rely-guarantee reasoning for causally consistent shared memory
• Specifying and reasoning about shared-variable concurrency
• Verifying correctness of persistent concurrent data structures
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• A wide-spectrum language for verification of programs on weak memory models
• Encoding fairness in a synchronous concurrent program algebra
• Reasoning about Separation Using Abstraction and Reification
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• Compositional analysis of C/C++ programs with veriSoft
• Local Symmetry and Compositional Verification
• Compositional verification of a communication protocol for a remotely operated aircraft
• Splitting atoms safely
• Proving linearizability with temporal logic
• Assumption/guarantee specifications in linear-time temporal logic
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• Balancing expressiveness in formal approaches to concurrency
• Conditions of contracts for separating responsibilities in heterogeneous systems
• Compositional Reasoning
• Elucidating concurrent algorithms via layers of abstraction and reification
• Fifty years of Hoare's logic
• Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
• Regression Verification for Multi-threaded Programs
• Semantic models of a timed distributed dataspace architecture
• Compositional reasoning using intervals and time reversal
• Guest editors' preface to special issue on interval temporal logics
• Verification of evolving software via component substitutability analysis
• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• An operational semantics for object-oriented concepts based on the class hierarchy
• Derivation of concurrent programs by stepwise scheduling of Event-B models
• Reasoning about goal-directed real-time teleo-reactive programs
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Interconnections between classes of sequentially compositional temporal formulas
• A Higher-Order Logic for Concurrent Termination-Preserving Refinement
• Compositional probabilistic verification through multi-objective model checking
• Compositionality Entails Sequentializability
• Certifying low-level programs with hardware interrupts and preemptive threads
• Generalised rely-guarantee concurrency: an algebraic foundation
• An explanatory presentation of composition rules for assumption- commitment specifications
• Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
• Title not available (Why is that?)
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
• Formal verification of concurrent programs with Read-write locks
• Certifying assembly programs with trails
• Designing a semantic model for a wide-spectrum language with concurrency
• Modular verification of multithreaded programs
• Compositional reasoning for shared-variable concurrent programs
• An application of temporal projection to interleaving concurrency
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• A compositional protocol verification using relativized bisimulation
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• A compositional axiomatization of statecharts
• Application of the composition principle to unity-like specifications
• The Composition of Event-B Models
• A verification-driven framework for iterative design of controllers
• Assume-guarantee reasoning with local specifications
• Composing leads-to properties
• A Program Construction and Verification Tool for Separation Logic

This page was built for publication: Tentative steps toward a development method for interfering programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3666252)