Data Refinement

DOI10.1017/CBO9780511663079zbMath0955.68076OpenAlexW4254136620MaRDI QIDQ4702189

Kai Engelhardt, Willem Paul de Roever

Publication date: 24 November 1999

Full work available at URL: https://doi.org/10.1017/cbo9780511663079

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (63)

Layout randomization and nondeterminism ⋮ Components as coalgebras: the refinement dimension ⋮ Evolution of rule-based programs ⋮ Allegories and Collagories for Transformation of Graph Structures Considered as Coalgebras ⋮ Logical relations and parametricity -- a Reynolds programme for category theory and programming languages ⋮ Levels of abstraction and the Turing test ⋮ Verifying data refinements using a model checker ⋮ An analysis of refinement in an abortive paradigm ⋮ The specification logic \(\nu \)Z ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Property transformation under specification change ⋮ Generalising the array split obfuscation ⋮ On using data abstractions for model checking refinements ⋮ Incompleteness of relational simulations in the blocking paradigm ⋮ Information flow in systems with schedulers. II: Refinement ⋮ Observational purity and encapsulation ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Composition mechanisms for retrenchment ⋮ Temporal-logic property preservation under Z refinement ⋮ Model evolution and refinement ⋮ A probability perspective ⋮ Simple feature engineering via neat default retrenchments ⋮ On the Purpose of Event-B Proof Obligations ⋮ Hybrid I/O automata. ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ The mechanical generation of fault trees for reactive systems via retrenchment. I. Combinational circuits ⋮ Secure Microkernels, State Monads and Scalable Refinement ⋮ Relational Concurrent Refinement: Automata ⋮ Data Refinement with Probability in Mind ⋮ Guarded Operations, Refinement and Simulation ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Completeness of ASM Refinement ⋮ More Relational Concurrent Refinement: Traces and Partial Relations ⋮ Layout Randomization and Nondeterminism ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ Completeness of fair ASM refinement ⋮ A hierarchy of failures-based models: theory and application ⋮ Retrenchment and refinement interworking: the tower theorems ⋮ Collagories: relation-algebraic reasoning for gluing constructions ⋮ Stronger compositions for retrenchments ⋮ Refactoring Object-Oriented Specifications with Data and Processes ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Model transformations across views ⋮ A Bibliography of Willem-Paul de Roever ⋮ Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules ⋮ Modelling Divergence in Relational Concurrent Refinement ⋮ Unnamed Item ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Concerned with the unprivileged: user programs in kernel refinement ⋮ Introducing extra operations in refinement ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ Philosophical Conceptions of Information ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ Relational concurrent refinement. II: Internal operations and outputs ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Category Theoretic Models of Data Refinement ⋮ Against digital ontology ⋮ Automated verification of refinement laws ⋮ Cogent: uniqueness types and certifying compilation ⋮ Soundness of data refinement for a higher-order imperative language ⋮ Generic Tools via General Refinement ⋮ State-level and value-level simulations in data refinement

This page was built for publication: Data Refinement