Tentative steps toward a development method for interfering programs
From MaRDI portal
Cited in
(80)- A compositional protocol verification using relativized bisimulation
- A compositional axiomatization of statecharts
- An explanatory presentation of composition rules for assumption- commitment specifications
- Composing leads-to properties
- Designing a semantic model for a wide-spectrum language with concurrency
- Verifying a concurrent garbage collector using a rely-guarantee methodology
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Semantic models of a timed distributed dataspace architecture
- Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
- Verifying correctness of persistent concurrent data structures: a sound and complete method
- 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
- Guest editors' preface to special issue on interval temporal logics
- Compositional reasoning using intervals and time reversal
- Fifty years of Hoare's logic
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A verification-driven framework for iterative design of controllers
- An application of temporal projection to interleaving concurrency
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Counterexample-guided abstraction refinement for symmetric concurrent programs
- Compositional verification of a communication protocol for a remotely operated aircraft
- Interconnections between classes of sequentially compositional temporal formulas
- Compositional analysis of C/C++ programs with veriSoft
- Assume-guarantee reasoning with local specifications
- Regression verification for multi-threaded programs
- Local symmetry and compositional verification
- A program construction and verification tool for separation logic
- A higher-order logic for concurrent termination-preserving refinement
- Compositionality Entails Sequentializability
- Compositional reasoning
- Compositional system security with interface-confined adversaries
- Generalised rely-guarantee concurrency: an algebraic foundation
- Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
- Formal verification of concurrent programs with Read-write locks
- Certifying assembly programs with trails
- The Composition of Event-B Models
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Compositional probabilistic verification through multi-objective model checking
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
- Transfer Principles for Reasoning About Concurrent Programs
- scientific article; zbMATH DE number 7444022 (Why is no real title available?)
- Protocol combinators for modeling, testing, and execution of distributed systems
- Application of the composition principle to unity-like specifications
- Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
- Reasoning about separation using abstraction and reification
- Proving linearizability with temporal logic
- Elucidating concurrent algorithms via layers of abstraction and reification
- Modular verification of multithreaded programs
- 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)
- A fine-grained semantics for arrays and pointers under weak memory models
- Asynchronous Cooperative Contracts for Cooperative Scheduling
- Rely-guarantee reasoning for causally consistent shared memory
- Specifying and reasoning about shared-variable concurrency
- A parametric rely-guarantee reasoning framework for concurrent reactive systems
- Verifying correctness of persistent concurrent data structures
- Extending rely-guarantee thinking to handle real-time scheduling
- Assumption/guarantee specifications in linear-time temporal logic
- A rely-guarantee-based simulation for cooperative semantics
- A generalised union of rely-guarantee and separation logic using permission algebras
- A general approach to under-approximate reasoning about concurrent programs
- Separability and non-determinizability of WSTS
- Compositional reasoning using the assumption-commitment paradigm
- Lazy compositional verication
- Deductive verification of modular systems
- The need for compositional proof systems: a survey
- Restructuring a concurrent refinement algebra
- The beauty of predicate automata
- Compositional reasoning for parametric probabilistic automata
- Concurrent Refinement Algebra and Rely Quotients
- ConcurrentHOL
- 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
- Certifying low-level programs with hardware interrupts and preemptive threads
- Splitting atoms safely
- Balancing expressiveness in formal approaches to concurrency
- Verification of evolving software via component substitutability analysis
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)
