Tentative steps toward a development method for interfering programs
From MaRDI portal
Publication:3666252
Cited in
(67)- Verifying correctness of persistent concurrent data structures: a sound and complete method
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A wide-spectrum language for verification of programs on weak memory models
- Encoding fairness in a synchronous concurrent program algebra
- Regression verification for multi-threaded programs
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Compositional analysis of C/C++ programs with veriSoft
- Splitting atoms safely
- Compositional verification of a communication protocol for a remotely operated aircraft
- Proving linearizability with temporal logic
- Extending rely-guarantee thinking to handle real-time scheduling
- Assumption/guarantee specifications in linear-time temporal logic
- Balancing expressiveness in formal approaches to concurrency
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Conditions of contracts for separating responsibilities in heterogeneous systems
- A higher-order logic for concurrent termination-preserving refinement
- 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
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
- Semantic models of a timed distributed dataspace architecture
- Reasoning about separation using abstraction and reification
- 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
- Compositional system security with interface-confined adversaries
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Interconnections between classes of sequentially compositional temporal formulas
- Protocol combinators for modeling, testing, and execution of distributed systems
- Compositional probabilistic verification through multi-objective model checking
- Certifying low-level programs with hardware interrupts and preemptive threads
- Compositionality Entails Sequentializability
- 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)
- A program construction and verification tool for separation logic
- scientific article; zbMATH DE number 7444022 (Why is no real title available?)
- Formal verification of concurrent programs with Read-write locks
- Certifying assembly programs with trails
- Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
- Designing a semantic model for a wide-spectrum language with concurrency
- Modular verification of multithreaded programs
- Asynchronous Cooperative Contracts for Cooperative Scheduling
- Compositional reasoning for shared-variable concurrent programs
- A compositional protocol verification using relativized bisimulation
- Verifying a concurrent garbage collector using a rely-guarantee methodology
- An application of temporal projection to interleaving concurrency
- A fine-grained semantics for arrays and pointers under weak memory models
- A compositional axiomatization of statecharts
- Counterexample-guided abstraction refinement for symmetric concurrent programs
- The Composition of Event-B Models
- Application of the composition principle to unity-like specifications
- A verification-driven framework for iterative design of controllers
- Local symmetry and compositional verification
- Transfer Principles for Reasoning About Concurrent Programs
- Assume-guarantee reasoning with local specifications
- An introduction to compositional methods for concurrency and their application to real-time.
- Composing leads-to properties
- 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
- Compositional reasoning
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)
