Recommendations
Cites work
- scientific article; zbMATH DE number 3614147 (Why is no real title available?)
- scientific article; zbMATH DE number 3303654 (Why is no real title available?)
- Protocol Verification via Projections
- Proving entailment between conceptual state specifications
- Proving the Correctness of Multiprocess Programs
- Recognizing safety and liveness
- Specifying Concurrent Program Modules
Cited in
(only showing first 100 items - show all)- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- New results on timed specifications
- On hierarchically developing reactive systems
- Verification, refinement and scheduling of real-time programs
- Bridging the gap between fair simulation and trace inclusion
- The mailbox problem
- Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
- Completeness of ASM refinement
- A distributed resource allocation algorithm for many processes
- Two implementation relations and the correctness of communicating replicated processes
- Fair simulation
- Simulation relations and applications in formal methods
- A new approach for active automata learning based on apartness
- Components as coalgebras: the refinement dimension
- On the limits of refinement-testing for model-checking CSP
- Relating trace refinement and linearizability
- A single complete rule for data refinement
- A general lock-free algorithm using compare-and-swap
- Predicate abstraction for hyperliveness verification
- Approximately satisfied properties of systems and simple language homomorphisms
- Specification and refinement of mobile systems in MTLA and mobile UML
- Synthesizing precise and useful commutativity conditions
- Specifying reversibility with \(\mathrm{TLA}^+\)
- Abstract semantic diffing of evolving concurrent programs
- Universal extensions to simulate specifications
- RustHorn: CHC-based verification for Rust programs
- A formal verification technique for behavioural model-to-model transformations
- Verification of a multiprocessor cache protocol using simulation relations and higher-order logic
- Requirements, specifications, and minimal refinement
- Layout randomization and nondeterminism
- Queue based mutual exclusion with linearly bounded overtaking
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- Progress in certifying hardware model checking results
- Action systems in incremental and aspect-oriented modeling
- Some extensions to propositional mean-value calculus: expressiveness and decidability
- UNITY and Büchi automata
- Automated verification and refinement for physical-layer protocols
- Towards applying the composition principle to verify a microkernel operating system
- Simulation Refinement for Concurrency Verification
- Completeness of fair ASM refinement
- Simulation refinement for concurrency verification
- Finite and infinite implementation of transition systems
- Software Verification of Hyperproperties Beyond k-Safety
- Byzantizing Paxos by refinement
- Assumption/guarantee specifications in linear-time temporal logic
- Liveness in timed and untimed systems
- Verifying visibility-based weak consistency
- Verification of schedulability for real-time programs
- Formal verification of a programming logic for a distributed programming language
- Specification and verification of concurrent programs through refinements
- A criterion for atomicity revisited
- Axioms for real-time logics
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Local abstraction refinement for probabilistic timed programs
- Decomposing data structure commutativity proofs with \(mn\)-differencing
- On the complexity of verifying concurrent transition systems
- Understanding, Explaining, and Deriving Refinement
- Layout Randomization and Nondeterminism
- Mutex needs fairness
- Combining Decision Procedures by (Model-)Equality Propagation
- Critique of the Lake Arrowhead three
- Refinement and state machine abstraction
- Combining decision procedures by (model-)equality propagation
- Invariance under stuttering in a temporal logic of actions
- Composition: a way to make proofs harder
- Compositional proofs for concurrent objects
- The need for compositional proof systems: a survey
- Why3-do: the way of harmonious distributed system proofs
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Resolution-based approach to compatibility analysis of interacting automata
- A theory of implementation and refinement in timed Petri nets
- On fairness notions in distributed systems. I: A characterization of implementability
- Using mappings to prove timing properties
- Property preserving abstractions for the verification of concurrent systems
- Efficient loop conditions for bounded model checking hyperproperties
- Liminf progress measures
- Splitting forward simulations to cope with liveness
- Synthesizing history and prophecy variables for symbolic model checking
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- Incompleteness of relational simulations in the blocking paradigm
- Refinement calculus: A basis for translation validation, debugging and certification
- Guarded transitions in evolving specifications
- Synthesis of Reactive(1) designs
- A formal theory of simulations between infinite automata
- On the complexity of verifying concurrent transition systems
- Fair simulation
- Set theory for verification. I: From foundations to functions
- Precise specification matching for adaptive reuse in embedded systems
- Generalized arrays for Stainless frames
- Network invariants for real-time systems
- scientific article; zbMATH DE number 1949612 (Why is no real title available?)
- Starvation-free mutual exclusion with semaphores
- Design and Verification of Fault-Tolerant Components
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Refinement verification of the lazy caching algorithm
- A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
- On the refinement of liveness properties of distributed systems
- Nonatomic dual bakery algorithm with bounded tokens
- Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
This page was built for publication: The existence of refinement mappings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q805251)
