The existence of refinement mappings
From MaRDI portal
Publication:805251
DOI10.1016/0304-3975(91)90224-PzbMath0728.68083OpenAlexW2132107743MaRDI QIDQ805251
Publication date: 1991
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(91)90224-p
Related Items
I/O automata in Isabelle/HOL, Simulation relations and applications in formal methods, Why3-do: the way of harmonious distributed system proofs, Liminf progress measures, Synthesizing history and prophecy variables for symbolic model checking, RHLE: modular deductive verification of relational \(\forall \exists\) properties, Fair simulation, Layout randomization and nondeterminism, Specification and refinement of mobile systems in MTLA and mobile UML, Components as coalgebras: the refinement dimension, New Results on Timed Specifications, Verifying Visibility-Based Weak Consistency, RustHorn: CHC-Based Verification for Rust Programs, Mutex needs fairness, Progress in certifying hardware model checking results, Refinement calculus: A basis for translation validation, debugging and certification, Precise specification matching for adaptive reuse in embedded systems, Property preserving abstractions for the verification of concurrent systems, Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos, Generalized arrays for Stainless frames, Comparative branching-time semantics for Markov chains, Verification of schedulability for real-time programs, Two implementation relations and the correctness of communicating replicated processes, Invariance under stuttering in a temporal logic of actions, A general lock-free algorithm using compare-and-swap, Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm, A distributed resource allocation algorithm for many processes, Resolution-based approach to compatibility analysis of interacting automata, A theory of implementation and refinement in timed Petri nets, A criterion for atomicity revisited, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, Assumption/guarantee specifications in linear-time temporal logic (extended abstract), A foundation for modular reasoning about safety and progress properties of state-based concurrent programs, Relating trace refinement and linearizability, Dynamic hierarchical reactive controller synthesis, On the limits of refinement-testing for model-checking CSP, Model-based construction and verification of critical systems using composition and partial refinement, Combining decision procedures by (model-)equality propagation, Synthesis of Reactive(1) designs, Synthesizing precise and useful commutativity conditions, Verifying atomic data types, Specifying reversibility with \(\mathrm{TLA}^+\), On hierarchically developing reactive systems, Starvation-free mutual exclusion with semaphores, Hume box calculus: Robust system development through software transformation, Action systems in incremental and aspect-oriented modeling, Compositional Abstraction in Real-Time Model Checking, Local abstraction refinement for probabilistic timed programs, The mailbox problem, Decomposing data structure commutativity proofs with \(mn\)-differencing, Assumption/guarantee specifications in linear-time temporal logic, Dynamic networks of heterogeneous timed machines, Approximately satisfied properties of systems and simple language homomorphisms, Conditions of contracts for separating responsibilities in heterogeneous systems, Simulation Refinement for Concurrency Verification, Completeness of ASM Refinement, Heterogeneous and asynchronous networks of timed systems, Operational specification with joint actions: Serializable databases, Specifying modules to satisfy interfaces: A state transition system approach, Critique of the Lake Arrowhead three, Minimal refinements of specifications in modal and temporal logics, A formal verification technique for behavioural model-to-model transformations, A single complete rule for data refinement, Verification of a multiprocessor cache protocol using simulation relations and higher-order logic, Universal extensions to simulate specifications, Using mappings to prove timing properties, Requirements, specifications, and minimal refinement, Finite and infinite implementation of transition systems, Queue based mutual exclusion with linearly bounded overtaking, Layout Randomization and Nondeterminism, Automated verification and refinement for physical-layer protocols, On the complexity of verifying concurrent transition systems, Simulation refinement for concurrency verification, Completeness of fair ASM refinement, Bridging the gap between fair simulation and trace inclusion, Minimal refinements of specifications in modal and temporal logics, Combining Decision Procedures by (Model-)Equality Propagation, Splitting forward simulations to cope with liveness, UNITY and Büchi automata, Axioms for real-time logics, Refinement and state machine abstraction, Refinement verification of the lazy caching algorithm, Counterexample-guided prophecy for model checking modulo the theory of arrays, Design and Verification of Fault-Tolerant Components, Network invariants for real-time systems, Temporal prophecy for proving temporal properties of infinite-state systems, Liveness in timed and untimed systems, Byzantizing Paxos by Refinement, Automatic analysis of DMA races using model checking and \(k\)-induction, On the refinement of liveness properties of distributed systems, Formal Verification for High-Assurance Behavioral Synthesis, Nonatomic dual bakery algorithm with bounded tokens, Formal verification of a programming logic for a distributed programming language, Abstract semantic diffing of evolving concurrent programs, Operating system verification---an overview, Linearizability on hardware weak memory models, Unnamed Item, Verification, refinement and scheduling of real-time programs, Programming interfaces and basic topology, On fairness notions in distributed systems. I: A characterization of implementability, Fair simulation, On the complexity of verifying concurrent transition systems, A formal theory of simulations between infinite automata, Understanding, Explaining, and Deriving Refinement, Specification and verification of concurrent programs through refinements, Set theory for verification. I: From foundations to functions
Cites Work
